1  /-
  2  Copyright (c) 2018 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Jens Wagemaker
  5  
  6  Associated and irreducible elements.
  7  -/
  8  import algebra.group data.multiset
src         └───────────┘ └───────────┘
  9  
 10  variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 11  open lattice
 12  
 13  /-- is unit -/
 14  def is_unit [monoid α] (a : α) : Prop := ∃u:units α, a = u
id                └────┘                      └───┘    
src               └────┘                        └───┘     
typ               └────┘                      └───┘    
 15  
 16  @[simp] lemma is_unit_unit [monoid α] (u : units α) : is_unit (u : α) := ⟨u, rfl⟩
id                               └────┘        └───┘     └─────┘             └─┘
src                              └────┘         └───┘      └─────┘                └─┘
typ                              └────┘        └───┘     └─────┘             └─┘
doc    └──┘                                                └─────┘
 17  
 18  theorem is_unit.mk0 [division_ring α] (x : α) (hx : x ≠ 0) : is_unit x := is_unit_unit (units.mk0 x hx)
id                        └───────────┘                       └─────┘     └──────────┘  └───────┘  └┘
src                       └───────────┘                          └─────┘      └──────────┘  └───────┘
typ                       └───────────┘                       └─────┘     └──────────┘  └───────┘  └┘
doc                                                               └─────┘                    └───────┘
 19  
 20  lemma is_unit.map [monoid α] [monoid β] (f : α →* β) {x : α} (h : is_unit x) : is_unit (f x) :=
id                      └────┘    └────┘         └┘               └─────┘     └─────┘   
src                     └────┘     └────┘           └┘                 └─────┘      └─────┘
typ                     └────┘    └────┘         └┘               └─────┘     └─────┘   
doc                                                 └┘                 └─────┘      └─────┘
 21  by rcases h with ⟨y, rfl⟩; exact is_unit_unit (units.map f y)
id                                   └──────────┘  └───────┘  
src     └─────┘ └────────────┘  └────┘└──────────┘ └───────┘  └─
typ     └─────┘└────────────┘  └────┘└──────────┘ └───────┘└─
doc     └─────┘ └────────────┘  └────┘                        └─
txt     └─────┘ └────────────┘  └────┘                        └─
par     └─────┘ └────────────┘  └────┘                        └─
pid            └────────────┘                               
st     └───────────────────────────────────────────────────────────
 22  
src  
typ  
doc  
txt  
par  
pid  
st   
 23  lemma is_unit.map' [monoid α] [monoid β] (f : α → β) {x : α} (h : is_unit x) [is_monoid_hom f] :
id                       └────┘    └────┘                         └─────┘    └───────────┘ 
src                      └────┘     └────┘                             └─────┘     └───────────┘
typ                      └────┘    └────┘                         └─────┘    └───────────┘ 
doc                                                                    └─────┘     └───────────┘
 24    is_unit (f x) :=
id     └─────┘   
src    └─────┘
typ    └─────┘   
doc    └─────┘
 25  h.map (monoid_hom.of f)
id   └──┘  └───────────┘ 
src   └──┘  └───────────┘
typ  └──┘  └───────────┘ 
doc         └───────────┘
 26  
 27  @[simp] theorem is_unit_zero_iff [semiring α] : is_unit (0 : α) ↔ (0:α) = 1 :=
id                                     └──────┘     └─────┘              
src                                    └──────┘      └─────┘                
typ                                    └──────┘     └─────┘              
doc    └──┘                                          └─────┘
 28  ⟨λ ⟨⟨_, a, (a0 : 0 * a = 1), _⟩, rfl⟩, by rwa zero_mul at a0,
id                                 └─┘          └──────┘
src                                 └─┘      └──┘└──────┘└────┘
typ                                └─┘      └──┘└──────┘└────┘
doc                                            └──┘        └────┘
txt                                            └──┘        └────┘
par                                            └──┘        └────┘
pid                                                       └────┘
st                                            └─────────────────┘
 29   λ h, begin
id      
typ     
st         └─────
 30    haveI := subsingleton_of_zero_eq_one _ h,
id              └─────────────────────────┘   
src    └───────┘└─────────────────────────┘└─┘
typ    └───────┘└─────────────────────────┘└─┘
doc    └───────┘└─────────────────────────┘└─┘
txt    └───────┘                           └─┘
par    └───────┘                           └─┘
pid         └─┘                           └─┘
st   ─────────────────────────────────────────┘└─
 31    refine ⟨⟨0, 0, _, _⟩, rfl⟩; apply subsingleton.elim
id                           └─┘         └───────────────┘
src    └─────┘  └───────────┘└─┘  └────┘└───────────────┘
typ    └─────┘  └───────────┘└─┘  └────┘└───────────────┘
doc    └─────┘  └───────────┘     └────┘                 
txt    └─────┘  └───────────┘     └────┘                 
par    └─────┘  └───────────┘     └────┘                 
pid            └───────────┘                           
st   ──────────────────────────────────────────────────────
 32   end⟩
src  
typ  
doc  
txt  
par  
pid  
st   └─┘
 33  
 34  @[simp] theorem not_is_unit_zero [nonzero_comm_ring α] : ¬ is_unit (0 : α) :=
id                                     └───────────────┘      └─────┘      
src                                    └───────────────┘       └─────┘
typ                                    └───────────────┘      └─────┘      
doc    └──┘                            └───────────────┘        └─────┘
 35  mt is_unit_zero_iff.1 zero_ne_one
id   └┘ └──────────────┘  └─────────┘
src  └┘ └──────────────┘  └─────────┘
typ  └┘ └──────────────┘  └─────────┘
 36  
 37  @[simp] theorem is_unit_one [monoid α] : is_unit (1:α) := ⟨1, rfl⟩
id                                └────┘     └─────┘             └─┘
src                               └────┘      └─────┘              └─┘
typ                               └────┘     └─────┘             └─┘
doc    └──┘                                   └─────┘
 38  
 39  theorem is_unit_of_mul_one [comm_monoid α] (a b : α) (h : a * b = 1) : is_unit a :=
id                               └─────────┘                          └─────┘ 
src                              └─────────┘                              └─────┘
typ                              └─────────┘                          └─────┘ 
doc                                                                         └─────┘
 40  ⟨units.mk_of_mul_eq_one a b h, rfl⟩
id    └────────────────────┘     └─┘
src   └────────────────────┘        └─┘
typ   └────────────────────┘     └─┘
 41  
 42  theorem is_unit_iff_exists_inv [comm_monoid α] {a : α} : is_unit a ↔ ∃ b, a * b = 1 :=
id                                   └─────────┘            └─────┘        
src                                  └─────────┘              └─────┘            
typ                                  └─────────┘            └─────┘        
doc                                                           └─────┘
 43  ⟨by rintro ⟨⟨a, b, hab, _⟩, rfl⟩; exact ⟨b, hab⟩,
id                                              └─┘
src      └──────────────────────────┘  └────┘  └┘   
typ      └──────────────────────────┘  └────┘ └┘└─┘
doc      └──────────────────────────┘  └────┘  └┘   
txt      └──────────────────────────┘  └────┘  └┘   
par      └──────────────────────────┘  └────┘  └┘   
pid            └────────────────────┘         └┘   
st      └───────────────────────────────────────────┘
 44   λ ⟨b, hab⟩, is_unit_of_mul_one _ b hab⟩
id        └─┘   └────────────────┘
src               └────────────────┘
typ       └─┘   └────────────────┘
 45  
 46  theorem is_unit_iff_exists_inv' [comm_monoid α] {a : α} : is_unit a ↔ ∃ b, b * a = 1 :=
id                                    └─────────┘            └─────┘        
src                                   └─────────┘              └─────┘            
typ                                   └─────────┘            └─────┘        
doc                                                            └─────┘
 47  by simp [is_unit_iff_exists_inv, mul_comm]
id            └────────────────────┘  └──────┘
src     └────┘└────────────────────┘└┘└──────┘└─
typ     └────┘└────────────────────┘└┘└──────┘└─
doc     └────┘                      └┘        └─
txt     └────┘                      └┘        └─
par     └────┘                      └┘        └─
pid                               └┘        
st     └────────────────────────────────────────
 48  
src  
typ  
doc  
txt  
par  
pid  
st   
 49  lemma is_unit_pow [monoid α] {a : α} (n : ℕ) : is_unit a → is_unit (a ^ n) :=
id                      └────┘                   └─────┘    └─────┘    
src                     └────┘                     └─────┘     └─────┘    
typ                     └────┘                   └─────┘    └─────┘    
doc                                                 └─────┘     └─────┘
 50  λ ⟨u, hu⟩, ⟨u ^ n, by simp *⟩
id                
src                       └────┘
typ                    └────┘
doc                        └────┘
txt                        └────┘
par                        └────┘
pid                            
st                        └─────┘
 51  
 52  @[simp] theorem units.is_unit_mul_units [monoid α] (a : α) (u : units α) :
id                                            └────┘               └───┘ 
src                                           └────┘                 └───┘
typ                                           └────┘               └───┘ 
doc    └──┘
 53    is_unit (a * u) ↔ is_unit a :=
id     └─────┘       └─────┘ 
src    └─────┘         └─────┘
typ    └─────┘       └─────┘ 
doc    └─────┘           └─────┘
 54  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
 55    (assume ⟨v, hv⟩,
id             
typ            
 56      have is_unit (a * ↑u * ↑u⁻¹), by existsi v * u⁻¹; rw [hv, units.coe_mul],
id            └─────┘      └┘                └┘      └┘  └───────────┘
src           └─────┘         └┘      └──────┘  └┘  └──┘  └┘└───────────┘
typ           └─────┘      └┘      └──────┘└┘  └──┘└┘└┘└───────────┘
doc           └─────┘                     └──────┘       └──┘  └┘             
txt                                       └──────┘       └──┘  └┘             
par                                       └──────┘       └──┘  └┘             
pid                                                       └┘  └┘             
st                                       └────────────────────┘└┘└─────────────┘
 57      by rwa [mul_assoc, units.mul_inv, mul_one] at this)
id               └───────┘  └───────────┘  └─────┘
src         └───┘└───────┘└┘└───────────┘└┘└─────┘└───────┘
typ         └───┘└───────┘└┘└───────────┘└┘└─────┘└───────┘
doc         └───┘         └┘             └┘       └───────┘
txt         └───┘         └┘             └┘       └───────┘
par         └───┘         └┘             └┘       └───────┘
pid            └┘         └┘             └┘       └──────┘
st         └─────────────┘└─────────────┘└───────┘└──────┘
 58    (assume ⟨v, hv⟩, hv.symm ▸ ⟨v * u, (units.coe_mul v u).symm⟩)
id               └┘     └───┘         └───────────┘    └──┘
src                       └───┘          └───────────┘     └──┘
typ              └┘     └───┘         └───────────┘    └──┘
 59  
 60  theorem is_unit_of_mul_is_unit_left {α} [comm_monoid α] {x y : α}
id                                            └─────────┘          
src                                           └─────────┘
typ                                           └─────────┘          
 61    (hu : is_unit (x * y)) : is_unit x :=
id           └─────┘         └─────┘ 
src          └─────┘           └─────┘
typ          └─────┘         └─────┘ 
doc          └─────┘            └─────┘
 62  let ⟨z, hz⟩ := is_unit_iff_exists_inv.1 hu in
id   └─┘           └────────────────────┘  └┘
src                 └────────────────────┘
typ  └─┘           └────────────────────┘  └┘
 63  is_unit_iff_exists_inv.2 ⟨y * z, by rwa ← mul_assoc⟩
id   └────────────────────┘                 └───────┘
src  └────────────────────┘            └────┘└───────┘
typ  └────────────────────┘           └────┘└───────┘
doc                                      └────┘
txt                                      └────┘
par                                      └────┘
pid                                         └─┘
st                                      └──────────────┘
 64  
 65  theorem is_unit_of_mul_is_unit_right {α} [comm_monoid α] {x y : α}
id                                             └─────────┘          
src                                            └─────────┘
typ                                            └─────────┘          
 66    (hu : is_unit (x * y)) : is_unit y :=
id           └─────┘         └─────┘ 
src          └─────┘           └─────┘
typ          └─────┘         └─────┘ 
doc          └─────┘            └─────┘
 67  @is_unit_of_mul_is_unit_left _ _ y x $ by rwa mul_comm
id    └─────────────────────────┘                └──────┘
src   └─────────────────────────┘              └──┘└──────┘
typ   └─────────────────────────┘            └──┘└──────┘
doc                                            └──┘        
txt                                            └──┘        
par                                            └──┘        
pid                                                       
st                                            └─────────────
 68  
src  
typ  
doc  
txt  
par  
pid  
st   
 69  theorem is_unit_iff_dvd_one [comm_semiring α] {x : α} : is_unit x ↔ x ∣ 1 :=
id                                └───────────┘            └─────┘    
src                               └───────────┘              └─────┘      
typ                               └───────────┘            └─────┘    
doc                                                          └─────┘
 70  ⟨by rintro ⟨u, rfl⟩; exact ⟨_, u.mul_inv.symm⟩,
id                                  └────────────┘
src      └─────────────┘  └────┘ └─┘└────────────┘
typ      └─────────────┘  └────┘ └─┘└────────────┘
doc      └─────────────┘  └────┘ └─┘              
txt      └─────────────┘  └────┘ └─┘              
par      └─────────────┘  └────┘ └─┘              
pid            └───────┘        └─┘              
st      └─────────────────────────────────────────┘
 71   λ ⟨y, h⟩, ⟨⟨x, y, h.symm, by rw [h, mul_comm]⟩, rfl⟩⟩
id                   └───┘           └──────┘    └─┘
src                      └───┘     └──┘ └┘└──────┘   └─┘
typ                  └───┘     └──┘└┘└──────┘   └─┘
doc                                └──┘ └┘        
txt                                └──┘ └┘        
par                                └──┘ └┘        
pid                                  └┘ └┘        
st                                └────┘└────────┘
 72  
 73  theorem is_unit_iff_forall_dvd [comm_semiring α] {x : α} :
id                                   └───────────┘        
src                                  └───────────┘
typ                                  └───────────┘        
 74    is_unit x ↔ ∀ y, x ∣ y :=
id     └─────┘         
src    └─────┘           
typ    └─────┘         
doc    └─────┘
 75  is_unit_iff_dvd_one.trans ⟨λ h y, dvd.trans h (one_dvd _), λ h, h _⟩
id   └─────────────────┘└────┘       └───────┘   └─────┘         
src  └─────────────────┘└────┘         └───────┘    └─────┘
typ  └─────────────────┘└────┘       └───────┘   └─────┘         
 76  
 77  theorem mul_dvd_of_is_unit_left [comm_semiring α] {x y z : α} (h : is_unit x) : x * y ∣ z ↔ y ∣ z :=
id                                    └───────────┘                   └─────┘             
src                                   └───────────┘                     └─────┘                 
typ                                   └───────────┘                   └─────┘             
doc                                                                     └─────┘
 78  ⟨dvd_trans (dvd_mul_left _ _),
id    └───────┘  └──────────┘
src   └───────┘  └──────────┘
typ   └───────┘  └──────────┘
 79   dvd_trans $ by simpa using mul_dvd_mul_right (is_unit_iff_dvd_one.1 h) y⟩
id    └───────┘                  └───────────────┘  └─────────────────┘     
src   └───────┘      └──────────┘└───────────────┘ └─────────────────┘└─┘ └┘
typ   └───────┘      └──────────┘└───────────────┘ └─────────────────┘└─┘└┘
doc                  └──────────┘                                     └─┘ └┘
txt                  └──────────┘                                     └─┘ └┘
par                  └──────────┘                                     └─┘ └┘
pid                       └────┘                                     └─┘ └┘
st                  └────────────────────────────────────────────────────────┘
 80  
 81  theorem mul_dvd_of_is_unit_right [comm_semiring α] {x y z : α} (h : is_unit y) : x * y ∣ z ↔ x ∣ z :=
id                                     └───────────┘                   └─────┘             
src                                    └───────────┘                     └─────┘                 
typ                                    └───────────┘                   └─────┘             
doc                                                                      └─────┘
 82  by rw [mul_comm, mul_dvd_of_is_unit_left h]
id          └──────┘  └─────────────────────┘ 
src     └──┘└──────┘└┘└─────────────────────┘ └─
typ     └──┘└──────┘└┘└─────────────────────┘└─
doc     └──┘        └┘                        └─
txt     └──┘        └┘                        └─
par     └──┘        └┘                        └─
pid       └┘        └┘                        
st     └───────────┘└─────────────────────────┘
 83  
src  
typ  
doc  
txt  
par  
pid  
st   
 84  @[simp] lemma unit_mul_dvd_iff [comm_semiring α] {a b : α} {u : units α} : (u : α) * a ∣ b ↔ a ∣ b :=
id                                   └───────────┘                 └───┘                  
src                                  └───────────┘                   └───┘                       
typ                                  └───────────┘                 └───┘                  
doc    └──┘
 85  mul_dvd_of_is_unit_left (is_unit_unit _)
id   └─────────────────────┘  └──────────┘
src  └─────────────────────┘  └──────────┘
typ  └─────────────────────┘  └──────────┘
 86  
 87  @[simp] lemma mul_unit_dvd_iff [comm_semiring α] {a b : α} {u : units α} : a * u ∣ b ↔ a ∣ b :=
id                                   └───────────┘                 └───┘             
src                                  └───────────┘                   └───┘                 
typ                                  └───────────┘                 └───┘             
doc    └──┘
 88  mul_dvd_of_is_unit_right (is_unit_unit _)
id   └──────────────────────┘  └──────────┘
src  └──────────────────────┘  └──────────┘
typ  └──────────────────────┘  └──────────┘
 89  
 90  theorem is_unit_of_dvd_unit {α} [comm_semiring α] {x y : α}
id                                    └───────────┘          
src                                   └───────────┘
typ                                   └───────────┘          
 91    (xy : x ∣ y) (hu : is_unit y) : is_unit x :=
id                     └─────┘     └─────┘ 
src                      └─────┘      └─────┘
typ                    └─────┘     └─────┘ 
doc                       └─────┘      └─────┘
 92  is_unit_iff_dvd_one.2 $ dvd_trans xy $ is_unit_iff_dvd_one.1 hu
id   └─────────────────┘    └───────┘ └┘   └─────────────────┘  └┘
src  └─────────────────┘    └───────┘      └─────────────────┘
typ  └─────────────────┘    └───────┘ └┘   └─────────────────┘  └┘
 93  
 94  @[simp] theorem is_unit_nat {n : ℕ} : is_unit n ↔ n = 1 :=
id                                        └─────┘    
src                                       └─────┘      
typ                                       └─────┘    
doc    └──┘                                └─────┘
 95  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
 96    (assume ⟨u, hu⟩, match n, u, hu, nat.units_eq_one u with _, _, rfl, rfl := rfl end)
id               └┘                  └──────────────┘                   └─┘    └─┘
src                                     └──────────────┘                   └─┘    └─┘
typ              └┘                  └──────────────┘                   └─┘    └─┘
 97    (assume h, h.symm ▸ ⟨1, rfl⟩)
id               └───┘      └─┘
src                └───┘      └─┘
typ              └───┘      └─┘
 98  
 99  theorem is_unit_int {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=
id                                └─────┘   └──────┘ 
src                               └─────┘     └──────┘ 
typ                               └─────┘   └──────┘ 
doc                                └─────┘
100  ⟨λ ⟨u, hu⟩, (int.units_eq_one_or u).elim (by simp *) (by simp *),
id              └─────────────────┘   └──┘
src               └─────────────────┘   └──┘      └────┘      └────┘
typ             └─────────────────┘   └──┘      └────┘      └────┘
doc                                               └────┘      └────┘
txt                                               └────┘      └────┘
par                                               └────┘      └────┘
pid                                                             
st                                               └─────┘     └─────┘
101    λ h, is_unit_iff_dvd_one.2 ⟨n, by rw [← int.nat_abs_mul_self, h]; refl⟩⟩
id         └─────────────────┘              └──────────────────┘  
src         └─────────────────┘         └────┘└──────────────────┘└┘   └──┘
typ        └─────────────────┘        └────┘└──────────────────┘└┘  └──┘
doc                                      └────┘                    └┘   └──┘
txt                                      └────┘                    └┘   └──┘
par                                      └────┘                    └┘   └──┘
pid                                        └──┘                    └┘ 
st                                      └─────────────────────────┘└─┘└────┘
102  
103  lemma is_unit_of_dvd_one [comm_semiring α] : ∀a ∣ 1, is_unit (a:α)
id                             └───────────┘            └─────┘   
src                            └───────────┘             └─────┘
typ                            └───────────┘            └─────┘   
doc                                                       └─────┘
104  | a ⟨b, eq⟩ := ⟨units.mk_of_mul_eq_one a b eq.symm, rfl⟩
id         └┘      └────────────────────┘       └───┘  └─┘
src          └┘      └────────────────────┘       └───┘  └─┘
typ        └┘      └────────────────────┘       └───┘  └─┘
105  
106  lemma dvd_and_not_dvd_iff [integral_domain α] {x y : α} :
id                              └─────────────┘          
src                             └─────────────┘
typ                             └─────────────┘          
107    x ∣ y ∧ ¬y ∣ x ↔ x ≠ 0 ∧ ∃ d : α, ¬ is_unit d ∧ y = x * d :=
id                         └─────┘       
src                              └─────┘         
typ                        └─────┘       
doc                                        └─────┘
108  ⟨λ ⟨⟨d, hd⟩, hyx⟩, ⟨λ hx0, by simpa [hx0] using hyx, ⟨d,
id         └┘   └─┘      └─┘            └─┘        └─┘
src                                └─────┘   └──────┘
typ        └┘   └─┘      └─┘     └─────┘└─┘└──────┘└─┘
doc                                └─────┘   └──────┘
txt                                └─────┘   └──────┘
par                                └─────┘   └──────┘
pid                                        └────┘
st                                └────────────────────┘
109      mt is_unit_iff_dvd_one.1 (λ ⟨e, he⟩, hyx ⟨e, by rw [hd, mul_assoc, ← he, mul_one]⟩), hd⟩⟩,
id       └┘ └─────────────────┘                           └┘  └───────┘    └┘  └─────┘
src      └┘ └─────────────────┘                         └──┘  └┘└───────┘└──┘  └┘└─────┘
typ      └┘ └─────────────────┘                       └──┘└┘└┘└───────┘└──┘└┘└┘└─────┘
doc                                                      └──┘  └┘         └──┘  └┘       
txt                                                      └──┘  └┘         └──┘  └┘       
par                                                      └──┘  └┘         └──┘  └┘       
pid                                                        └┘  └┘         └──┘  └┘       
st                                                      └─────┘└─────────┘└────┘└───────┘
110    λ ⟨hx0, d, hdu, hdx⟩, ⟨⟨d, hdx⟩, λ ⟨e, he⟩, hdu (is_unit_of_dvd_one _
id       └─┘    └─┘  └─┘                            └────────────────┘
src                                                     └────────────────┘
typ      └─┘    └─┘  └─┘                            └────────────────┘
111      ⟨e, (domain.mul_left_inj hx0).1 $ by conv {to_lhs, rw [he, hdx]};simp [mul_assoc]⟩)⟩⟩
id            └─────────────────┘                              └┘  └─┘         └───────┘
src           └─────────────────┘            └────┘└────┘└┘└──┘  └┘    └────┘└───────┘
typ           └─────────────────┘            └────┘└────┘└┘└──┘└┘└┘└─┘ └────┘└───────┘
doc           └─────────────────┘                                         └────┘         
txt                                           └────┘└────┘└┘└──┘  └┘    └────┘         
par                                           └────┘└────┘└┘└──┘  └┘    └────┘         
pid                                               └───────────┘  └┘   └┘              
st                                           └─────┘└────┘└──────┘└───┘ └┘└──────────────┘
112  
113  lemma pow_dvd_pow_iff [integral_domain α] {x : α} {n m : ℕ} (h0 : x ≠ 0) (h1 : ¬ is_unit x) :
id                          └─────────────┘                                     └─────┘ 
src                         └─────────────┘                                        └─────┘
typ                         └─────────────┘                                     └─────┘ 
doc                                                                                   └─────┘
114    x ^ n ∣ x ^ m ↔ n ≤ m :=
id               
src                  
typ              
115  begin
st   └─────
116    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
117    { intro h, rw [← not_lt], intro hmn, apply h1,
id                      └────┘
src      └─────┘  └────┘└────┘  └───────┘  └────┘
typ      └─────┘  └────┘└────┘  └───────┘  └────┘
doc      └─────┘  └────┘        └───────┘  └────┘
txt      └─────┘  └────┘        └───────┘  └────┘
par      └─────┘  └────┘        └───────┘  └────┘
pid           └┘    └──┘             └──┘       
st   ───┘└─────┘└────────────┘└──────────┘└────────┘└─
118      have : x * x ^ m ∣ 1 * x ^ m,
id                              
src      └─────┘   └─┘   
typ      └─────┘   └─┘  
doc      └─────┘      └─┘   
txt      └─────┘      └─┘   
par      └─────┘      └─┘   
pid      └───┘└┘      └─┘   
st   ───────────────────────────────┘└─
119      { rw [← pow_succ, one_mul], exact dvd_trans (pow_dvd_pow _ (nat.succ_le_of_lt hmn)) h },
id               └──────┘  └─────┘         └───────┘  └─────────┘    └───────────────┘ └─┘   
src        └────┘└──────┘└┘└─────┘  └────┘└───────┘ └─────────┘└─┘ └───────────────┘   └─┘ 
typ        └────┘└──────┘└┘└─────┘  └────┘└───────┘ └─────────┘└─┘ └───────────────┘└─┘└─┘
doc        └────┘        └┘         └────┘                     └─┘                     └─┘ 
txt        └────┘        └┘         └────┘                     └─┘                     └─┘ 
par        └────┘        └┘         └────┘                     └─┘                     └─┘ 
pid          └──┘        └┘                                   └─┘                     └─┘ 
st   ─────┘└────────────┘└───────┘└───────────────────────────────────────────────────────────┘└┘
120      rwa [mul_dvd_mul_iff_right, ← is_unit_iff_dvd_one] at this, apply pow_ne_zero m h0 },
id            └───────────────────┘    └─────────────────┘                 └─────────┘  └┘
src      └───┘└───────────────────┘└──┘└─────────────────┘└───────┘  └────┘└─────────┘   
typ      └───┘└───────────────────┘└──┘└─────────────────┘└───────┘  └────┘└─────────┘└┘
doc      └───┘└───────────────────┘└──┘                   └───────┘  └────┘              
txt      └───┘                     └──┘                   └───────┘  └────┘              
par      └───┘                     └──┘                   └───────┘  └────┘              
pid         └┘                     └──┘                   └──────┘                     
st   ─────────────────────────────┘└─────────────────────┘└──────┘└───────────────────────┘└┘
121    { apply pow_dvd_pow }
id             └─────────┘
src      └────┘└─────────┘
typ      └────┘└─────────┘
doc      └────┘           
txt      └────┘           
par      └────┘           
pid                      
st   ─────────────────────┘└─
122  end
st   ──┘
123  
124  /-- prime element of a semiring -/
125  def prime [comm_semiring α] (p : α) : Prop :=
id              └───────────┘        
src             └───────────┘
typ             └───────────┘        
126  p ≠ 0 ∧ ¬ is_unit p ∧ (∀a b, p ∣ a * b → p ∣ a ∨ p ∣ b)
id         └─────┘                     
src         └─────┘                             
typ        └─────┘                     
doc            └─────┘
127  
128  namespace prime
129  
130  lemma ne_zero [comm_semiring α] {p : α} (hp : prime p) : p ≠ 0 :=
id                  └───────────┘                └───┘      
src                 └───────────┘                  └───┘        
typ                 └───────────┘                └───┘      
doc                                                └───┘
131  hp.1
id   └┘
src    
typ  └┘
132  
133  lemma not_unit [comm_semiring α] {p : α} (hp : prime p) : ¬ is_unit p :=
id                   └───────────┘                └───┘      └─────┘ 
src                  └───────────┘                  └───┘       └─────┘
typ                  └───────────┘                └───┘      └─────┘ 
doc                                                 └───┘        └─────┘
134  hp.2.1
id   └┘ 
src     
typ  └┘ 
135  
136  lemma div_or_div [comm_semiring α] {p : α} (hp : prime p) {a b : α} (h : p ∣ a * b) :
id                     └───────────┘                └───┘                     
src                    └───────────┘                  └───┘                        
typ                    └───────────┘                └───┘                     
doc                                                   └───┘
137    p ∣ a ∨ p ∣ b :=
id           
src            
typ          
138  hp.2.2 a b h
id   └┘     
src     
typ  └┘     
139  
140  end prime
141  
142  @[simp] lemma not_prime_zero [comm_semiring α] : ¬ prime (0 : α) :=
id                                 └───────────┘      └───┘      
src                                └───────────┘       └───┘
typ                                └───────────┘      └───┘      
doc    └──┘                                             └───┘
143  λ h, h.ne_zero rfl
id       └──────┘ └─┘
src        └──────┘ └─┘
typ      └──────┘ └─┘
144  
145  @[simp] lemma not_prime_one [comm_semiring α] : ¬ prime (1 : α) :=
id                                └───────────┘      └───┘      
src                               └───────────┘       └───┘
typ                               └───────────┘      └───┘      
doc    └──┘                                            └───┘
146  λ h, h.not_unit is_unit_one
id       └───────┘ └─────────┘
src        └───────┘ └─────────┘
typ      └───────┘ └─────────┘
147  
148  lemma exists_mem_multiset_dvd_of_prime [comm_semiring α] {s : multiset α} {p : α} (hp : prime p) :
id                                           └───────────┘        └──────┘                └───┘ 
src                                          └───────────┘         └──────┘                  └───┘
typ                                          └───────────┘        └──────┘                └───┘ 
doc                                                                └──────┘                  └───┘
149    p ∣ s.prod → ∃a∈s, p ∣ a :=
id       └───┘       
src        └───┘         
typ      └───┘       
doc         └───┘
150  multiset.induction_on s (assume h, (hp.not_unit $ is_unit_of_dvd_one _ h).elim) $
id   └───────────────────┘             └┘└───────┘   └────────────────┘    └──┘
src  └───────────────────┘                 └───────┘   └────────────────┘     └──┘
typ  └───────────────────┘             └┘└───────┘   └────────────────┘    └──┘
151  assume a s ih h,
id            └┘ 
typ           └┘ 
152    have p ∣ a * s.prod, by simpa using h,
id              └───┘                 
src                └───┘     └──────────┘
typ             └───┘     └──────────┘
doc                  └───┘     └──────────┘
txt                            └──────────┘
par                            └──────────┘
pid                                 └────┘
st                            └────────────┘
153    match hp.div_or_div this with
id           └┘└─────────┘ └──┘
src            └─────────┘
typ          └┘└─────────┘ └──┘
154    | or.inl h := ⟨a, multiset.mem_cons_self a s, h⟩
id       └────┘        └────────────────────┘  
src      └────┘          └────────────────────┘
typ      └────┘        └────────────────────┘  
155    | or.inr h := let ⟨a, has, h⟩ := ih h in ⟨a, multiset.mem_cons_of_mem has, h⟩
id       └────┘     └─┘    └─┘       └┘          └──────────────────────┘
src      └────┘                                     └──────────────────────┘
typ      └────┘     └─┘    └─┘       └┘          └──────────────────────┘
156    end
157  
158  /-- `irreducible p` states that `p` is non-unit and only factors into units.
159  
160  We explicitly avoid stating that `p` is non-zero, this would require a semiring. Assuming only a
161  monoid allows us to reuse irreducible for associated elements.
162  -/
163  @[class] def irreducible [monoid α] (p : α) : Prop :=
id                             └────┘        
src                            └────┘
typ                            └────┘        
164  ¬ is_unit p ∧ ∀a b, p = a * b → is_unit a ∨ is_unit b
id    └─────┘              └─────┘   └─────┘ 
src   └─────┘                    └─────┘    └─────┘
typ   └─────┘              └─────┘   └─────┘ 
doc    └─────┘                       └─────┘     └─────┘
165  
166  namespace irreducible
167  
168  lemma not_unit [monoid α] {p : α} (hp : irreducible p) : ¬ is_unit p :=
id                   └────┘                └─────────┘      └─────┘ 
src                  └────┘                  └─────────┘       └─────┘
typ                  └────┘                └─────────┘      └─────┘ 
doc                                          └─────────┘        └─────┘
169  hp.1
id   └┘
src    
typ  └┘
170  
171  lemma is_unit_or_is_unit [monoid α] {p : α} (hp : irreducible p) {a b : α} (h : p = a * b) :
id                             └────┘                └─────────┘                     
src                            └────┘                  └─────────┘                        
typ                            └────┘                └─────────┘                     
doc                                                    └─────────┘
172    is_unit a ∨ is_unit b :=
id     └─────┘   └─────┘ 
src    └─────┘    └─────┘
typ    └─────┘   └─────┘ 
doc    └─────┘     └─────┘
173  hp.2 a b h
id   └┘    
src    
typ  └┘    
174  
175  end irreducible
176  
177  @[simp] theorem not_irreducible_one [monoid α] : ¬ irreducible (1 : α) :=
id                                        └────┘      └─────────┘      
src                                       └────┘       └─────────┘
typ                                       └────┘      └─────────┘      
doc    └──┘                                             └─────────┘
178  by simp [irreducible]
id            └─────────┘
src     └────┘└─────────┘└─
typ     └────┘└─────────┘└─
doc     └────┘└─────────┘└─
txt     └────┘           └─
par     └────┘           └─
pid                    
st     └───────────────────
179  
src  
typ  
doc  
txt  
par  
pid  
st   
180  @[simp] theorem not_irreducible_zero [semiring α] : ¬ irreducible (0 : α)
id                                         └──────┘      └─────────┘      
src                                        └──────┘       └─────────┘
typ                                        └──────┘      └─────────┘      
doc    └──┘                                                └─────────┘
181  | ⟨hn0, h⟩ := have is_unit (0:α) ∨ is_unit (0:α), from h 0 0 ((mul_zero 0).symm),
id      └─┘            └─────┘       └─────┘                    └──────┘   └──┘
src                     └─────┘        └─────┘                     └──────┘   └──┘
typ     └─┘            └─────┘       └─────┘                    └──────┘   └──┘
doc                     └─────┘         └─────┘
182    this.elim hn0 hn0
id     └──┘└───┘
src        └───┘
typ    └──┘└───┘
183  
184  theorem irreducible.ne_zero [semiring α] : ∀ {p:α}, irreducible p → p ≠ 0
id                                └──────┘            └─────────┘     
src                               └──────┘               └─────────┘       
typ                               └──────┘            └─────────┘     
doc                                                      └─────────┘
185  | _ hp rfl := not_irreducible_zero hp
id       └┘ └─┘    └──────────────────┘
src         └─┘    └──────────────────┘
typ      └┘ └─┘    └──────────────────┘
186  
187  theorem of_irreducible_mul {α} [monoid α] {x y : α} :
id                                   └────┘          
src                                  └────┘
typ                                  └────┘          
188    irreducible (x * y) → is_unit x ∨ is_unit y
id     └─────────┘       └─────┘   └─────┘ 
src    └─────────┘          └─────┘    └─────┘
typ    └─────────┘       └─────┘   └─────┘ 
doc    └─────────┘           └─────┘     └─────┘
189  | ⟨_, h⟩ := h _ _ rfl
id                    └─┘
src                    └─┘
typ                   └─┘
190  
191  theorem irreducible_or_factor {α} [monoid α] (x : α) (h : ¬ is_unit x) :
id                                      └────┘                └─────┘ 
src                                     └────┘                  └─────┘
typ                                     └────┘                └─────┘ 
doc                                                              └─────┘
192    irreducible x ∨ ∃ a b, ¬ is_unit a ∧ ¬ is_unit b ∧ a * b = x :=
id     └─────────┘       └─────┘    └─────┘       
src    └─────────┘          └─────┘     └─────┘         
typ    └─────────┘       └─────┘    └─────┘       
doc    └─────────┘              └─────┘       └─────┘
193  begin
st   └─────
194    haveI := classical.dec,
id              └───────────┘
src    └───────┘└───────────┘
typ    └───────┘└───────────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid         └─┘
st   ───────────────────────┘└─
195    refine or_iff_not_imp_right.2 (λ H, _),
id            └──────────────────┘
src    └─────┘└──────────────────┘└─┘  └────┘
typ    └─────┘└──────────────────┘└─┘  └────┘
doc    └─────┘                    └─┘  └────┘
txt    └─────┘                    └─┘  └────┘
par    └─────┘                    └─┘  └────┘
pid                              └─┘  └────┘
st   ───────────────────────────────────────┘└─
196    simp [h, irreducible] at H ⊢,
id             └─────────┘
src    └────┘ └┘└─────────┘└──────┘
typ    └────┘└┘└─────────┘└──────┘
doc    └────┘ └┘└─────────┘└──────┘
txt    └────┘ └┘           └──────┘
par    └────┘ └┘           └──────┘
pid         └┘           └────┘
st   ─────────────────────────────┘└─
197    refine λ a b h, classical.by_contradiction $ λ o, _,
id                     └────────────────────────┘
src    └─────┘ └──────┘└────────────────────────┘  └───┘
typ    └─────┘ └──────┘└────────────────────────┘  └───┘
doc    └─────┘ └──────┘                            └───┘
txt    └─────┘ └──────┘                            └───┘
par    └─────┘ └──────┘                            └───┘
pid           └──────┘                            └───┘
st   ────────────────────────────────────────────────────┘└─
198    simp [not_or_distrib] at o,
id           └────────────┘
src    └────┘└────────────┘└────┘
typ    └────┘└────────────┘└────┘
doc    └────┘              └────┘
txt    └────┘              └────┘
par    └────┘              └────┘
pid                      └──┘
st   ───────────────────────────┘└─
199    exact H _ o.1 _ o.2 h.symm
id                       └────┘
src    └────┘ └─┘ └───┘ └─┘└────┘
typ    └────┘└─┘ └───┘└─┘└────┘
doc    └────┘ └─┘ └───┘ └─┘      
txt    └────┘ └─┘ └───┘ └─┘      
par    └────┘ └─┘ └───┘ └─┘      
pid          └─┘ └───┘ └─┘      
st   ────────────────────────────┘
200  end
st   └─┘
201  
202  lemma irreducible_of_prime [integral_domain α] {p : α} (hp : prime p) : irreducible p :=
id                               └─────────────┘                └───┘     └─────────┘ 
src                              └─────────────┘                  └───┘      └─────────┘
typ                              └─────────────┘                └───┘     └─────────┘ 
doc                                                               └───┘      └─────────┘
203  ⟨hp.not_unit, λ a b hab,
id    └┘└───────┘      └─┘
src     └───────┘
typ   └┘└───────┘      └─┘
204    (show a * b ∣ a ∨ a * b ∣ b, from hab ▸ hp.div_or_div (hab ▸ (dvd_refl _))).elim
id                            └─┘  └┘└─────────┘  └─┘   └──────┘     └──┘
src                                        └─────────┘        └──────┘     └──┘
typ                           └─┘  └┘└─────────┘  └─┘   └──────┘     └──┘
205      (λ ⟨x, hx⟩, or.inr (is_unit_iff_dvd_one.2
id                 └────┘  └─────────────────┘
src                  └────┘  └─────────────────┘
typ                └────┘  └─────────────────┘
206        ⟨x, (domain.mul_left_inj (show a ≠ 0, from λ h, by simp [*, prime] at *)).1
id              └─────────────────┘                                 └───┘        
src             └─────────────────┘                          └───────┘└───┘└────┘  
typ             └─────────────────┘                        └───────┘└───┘└────┘  
doc             └─────────────────┘                           └───────┘└───┘└────┘
txt                                                           └───────┘     └────┘
par                                                           └───────┘     └────┘
pid                                                               └──┘     └──┘
st                                                           └───────────────────┘
207          $ by conv {to_lhs, rw hx}; simp [mul_comm, mul_assoc, mul_left_comm]⟩))
id                                 └┘         └──────┘  └───────┘  └───────────┘
src               └────┘└────┘└┘└─┘    └────┘└──────┘└┘└───────┘└┘└───────────┘
typ               └────┘└────┘└┘└─┘└┘  └────┘└──────┘└┘└───────┘└┘└───────────┘
doc                                     └────┘        └┘         └┘             
txt               └────┘└────┘└┘└─┘    └────┘        └┘         └┘             
par               └────┘└────┘└┘└─┘    └────┘        └┘         └┘             
pid                   └──────────┘                └┘         └┘             
st               └─────┘└────┘└─────┘└┘└────────────────────────────────────────┘
208      (λ ⟨x, hx⟩, or.inl (is_unit_iff_dvd_one.2
id                 └────┘  └─────────────────┘
src                  └────┘  └─────────────────┘
typ                └────┘  └─────────────────┘
209        ⟨x, (domain.mul_left_inj (show b ≠ 0, from λ h, by simp [*, prime] at *)).1
id              └─────────────────┘                                 └───┘        
src             └─────────────────┘                          └───────┘└───┘└────┘  
typ             └─────────────────┘                        └───────┘└───┘└────┘  
doc             └─────────────────┘                           └───────┘└───┘└────┘
txt                                                           └───────┘     └────┘
par                                                           └───────┘     └────┘
pid                                                               └──┘     └──┘
st                                                           └───────────────────┘
210          $ by conv {to_lhs, rw hx}; simp [mul_comm, mul_assoc, mul_left_comm]⟩))⟩
id                                 └┘         └──────┘  └───────┘  └───────────┘
src               └────┘└────┘└┘└─┘    └────┘└──────┘└┘└───────┘└┘└───────────┘
typ               └────┘└────┘└┘└─┘└┘  └────┘└──────┘└┘└───────┘└┘└───────────┘
doc                                     └────┘        └┘         └┘             
txt               └────┘└────┘└┘└─┘    └────┘        └┘         └┘             
par               └────┘└────┘└┘└─┘    └────┘        └┘         └┘             
pid                   └──────────┘                └┘         └┘             
st               └─────┘└────┘└─────┘└┘└────────────────────────────────────────┘
211  
212  lemma succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul [integral_domain α] {p : α} (hp : prime p) {a b : α}
id                                                   └─────────────┘                └───┘          
src                                                  └─────────────┘                  └───┘
typ                                                  └─────────────┘                └───┘          
doc                                                                                   └───┘
213    {k l : ℕ} : p ^ k ∣ a → p ^ l ∣ b → p ^ ((k + l) + 1) ∣ a * b →
id                                             
src                                                     
typ                                            
214    p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b :=
id                         
src                            
typ                        
215  λ ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩,
id                 
typ                
216  have h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z),
id                                      
src                                            
typ                                     
217    by simpa [mul_comm, _root_.pow_add, hx, hy, mul_assoc, mul_left_comm] using hz,
id               └──────┘  └────────────┘  └┘  └┘  └───────┘  └───────────┘        └┘
src       └─────┘└──────┘└┘└────────────┘└┘  └┘  └┘└───────┘└┘└───────────┘└──────┘
typ       └─────┘└──────┘└┘└────────────┘└┘└┘└┘└┘└┘└───────┘└┘└───────────┘└──────┘└┘
doc       └─────┘        └┘              └┘  └┘  └┘         └┘             └──────┘
txt       └─────┘        └┘              └┘  └┘  └┘         └┘             └──────┘
par       └─────┘        └┘              └┘  └┘  └┘         └┘             └──────┘
pid                    └┘              └┘  └┘  └┘         └┘             └────┘
st       └──────────────────────────────────────────────────────────────────────────┘
218  have hp0: p ^ (k + l) ≠ 0, from pow_ne_zero _ hp.ne_zero,
id                             └─────────┘   └┘└──────┘
src                               └─────────┘     └──────┘
typ                            └─────────┘   └┘└──────┘
219  have hpd : p ∣ x * y, from ⟨z, by rwa [domain.mul_left_inj hp0] at h⟩,
id                                       └─────────────────┘ └─┘
src                                  └───┘└─────────────────┘   └────┘
typ                                 └───┘└─────────────────┘└─┘└────┘
doc                                    └───┘└─────────────────┘   └────┘
txt                                    └───┘                      └────┘
par                                    └───┘                      └────┘
pid                                       └┘                      └───┘
st                                    └───────────────────────────┘└───┘
220  (hp.div_or_div hpd).elim
id    └┘└─────────┘ └─┘ └──┘
src     └─────────┘     └──┘
typ   └┘└─────────┘ └─┘ └──┘
221    (λ ⟨d, hd⟩, or.inl ⟨d, by simp [*, _root_.pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
id               └────┘                 └─────────────┘  └──────┘  └───────────┘  └───────┘
src                └────┘        └───────┘└─────────────┘└┘└──────┘└┘└───────────┘└┘└───────┘
typ              └────┘        └───────┘└─────────────┘└┘└──────┘└┘└───────────┘└┘└───────┘
doc                              └───────┘               └┘        └┘             └┘         
txt                              └───────┘               └┘        └┘             └┘         
par                              └───────┘               └┘        └┘             └┘         
pid                                  └──┘               └┘        └┘             └┘         
st                              └────────────────────────────────────────────────────────────┘
222    (λ ⟨d, hd⟩, or.inr ⟨d, by simp [*, _root_.pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
id               └────┘                 └─────────────┘  └──────┘  └───────────┘  └───────┘
src                └────┘        └───────┘└─────────────┘└┘└──────┘└┘└───────────┘└┘└───────┘
typ              └────┘        └───────┘└─────────────┘└┘└──────┘└┘└───────────┘└┘└───────┘
doc                              └───────┘               └┘        └┘             └┘         
txt                              └───────┘               └┘        └┘             └┘         
par                              └───────┘               └┘        └┘             └┘         
pid                                  └──┘               └┘        └┘             └┘         
st                              └────────────────────────────────────────────────────────────┘
223  
224  def associated [monoid α] (x y : α) : Prop := ∃u:units α, x * u = y
id                   └────┘                        └───┘      
src                  └────┘                          └───┘        
typ                  └────┘                        └───┘      
225  
226  local infix ` ~ᵤ ` : 50 := associated
id                              └────────┘
src                             └────────┘
typ                             └────────┘
227  
228  namespace associated
229  
230  @[refl] protected theorem refl [monoid α] (x : α) : x ~ᵤ x := ⟨1, by simp⟩
id                                   └────┘             └┘ 
src    └──┘                          └────┘                └┘             └──┘
typ                                  └────┘             └┘            └──┘
doc    └──┘                                                               └──┘
txt                                                                       └──┘
par                                                                       └──┘
st                                                                       └───┘
231  
232  @[symm] protected theorem symm [monoid α] : ∀{x y : α}, x ~ᵤ y → y ~ᵤ x
id                                   └────┘                └┘     └┘ 
src    └──┘                          └────┘                   └┘       └┘
typ                                  └────┘                └┘     └┘ 
doc    └──┘
233  | x _ ⟨u, rfl⟩ := ⟨u⁻¹, by rw [mul_assoc, units.mul_inv, mul_one]⟩
id            └─┘       └┘         └───────┘  └───────────┘  └─────┘
src            └─┘       └┘     └──┘└───────┘└┘└───────────┘└┘└─────┘
typ           └─┘       └┘     └──┘└───────┘└┘└───────────┘└┘└─────┘
doc                             └──┘         └┘             └┘       
txt                             └──┘         └┘             └┘       
par                             └──┘         └┘             └┘       
pid                               └┘         └┘             └┘       
st                             └────────────┘└─────────────┘└───────┘
234  
235  @[trans] protected theorem trans [monoid α] : ∀{x y z : α}, x ~ᵤ y → y ~ᵤ z → x ~ᵤ z
id                                     └────┘                  └┘     └┘     └┘ 
src    └───┘                           └────┘                     └┘       └┘       └┘
typ                                    └────┘                  └┘     └┘     └┘ 
doc    └───┘
236  | x _ _ ⟨u, rfl⟩ ⟨v, rfl⟩ := ⟨u * v, by rw [units.coe_mul, mul_assoc]⟩
id                      └─┘                   └───────────┘  └───────┘
src                       └─┘               └──┘└───────────┘└┘└───────┘
typ                     └─┘               └──┘└───────────┘└┘└───────┘
doc                                          └──┘             └┘         
txt                                          └──┘             └┘         
par                                          └──┘             └┘         
pid                                            └┘             └┘         
st                                          └────────────────┘└─────────┘
237  
238  protected def setoid (α : Type*) [monoid α] : setoid α :=
id                                     └────┘     └────┘ 
src                                    └────┘      └────┘
typ                                    └────┘     └────┘ 
239  { r := associated, iseqv := ⟨associated.refl, λa b, associated.symm, λa b c, associated.trans⟩ }
id          └────────┘            └─────────────┘      └─────────────┘       └──────────────┘
src         └────────┘            └─────────────┘        └─────────────┘          └──────────────┘
typ         └────────┘            └─────────────┘      └─────────────┘       └──────────────┘
240  
241  end associated
242  
243  local attribute [instance] associated.setoid
id                              └───────────────┘
src                             └───────────────┘
typ                             └───────────────┘
244  
245  theorem unit_associated_one [monoid α] {u : units α} : (u : α) ~ᵤ 1 := ⟨u⁻¹, units.mul_inv u⟩
id                                └────┘        └───┘           └┘       └┘  └───────────┘ 
src                               └────┘         └───┘              └┘        └┘  └───────────┘
typ                               └────┘        └───┘           └┘       └┘  └───────────┘ 
246  
247  theorem associated_one_iff_is_unit [monoid α] {a : α} : (a : α) ~ᵤ 1 ↔ is_unit a :=
id                                       └────┘                  └┘    └─────┘ 
src                                      └────┘                      └┘    └─────┘
typ                                      └────┘                  └┘    └─────┘ 
doc                                                                         └─────┘
248  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
249    (assume h, let ⟨c, h⟩ := h.symm in h ▸ ⟨c, one_mul _⟩)
id               └─┘         └───┘           └─────┘
src                              └───┘           └─────┘
typ              └─┘         └───┘           └─────┘
250    (assume ⟨c, h⟩, associated.symm ⟨c, by simp [h]⟩)
id                   └─────────────┘              
src                    └─────────────┘        └────┘ 
typ                  └─────────────┘        └────┘
doc                                           └────┘ 
txt                                           └────┘ 
par                                           └────┘ 
pid                                                
st                                           └───────┘
251  
252  theorem associated_zero_iff_eq_zero [comm_semiring α] (a : α) : a ~ᵤ 0 ↔ a = 0 :=
id                                        └───────────┘             └┘     
src                                       └───────────┘                └┘      
typ                                       └───────────┘             └┘     
253  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
254    (assume h, let ⟨u, h⟩ := h.symm in by simpa using h.symm)
id               └─┘           └───┘                   └────┘
src                              └───┘       └──────────┘└────┘
typ              └─┘           └───┘       └──────────┘└────┘
doc                                          └──────────┘
txt                                          └──────────┘
par                                          └──────────┘
pid                                               └────┘
st                                          └─────────────────┘
255    (assume h, h ▸ associated.refl a)
id                 └─────────────┘ 
src                  └─────────────┘
typ                └─────────────┘ 
256  
257  theorem associated_one_of_mul_eq_one [comm_monoid α] {a : α} (b : α) (hab : a * b = 1) : a ~ᵤ 1 :=
id                                         └─────────┘                                  └┘
src                                        └─────────┘                                        └┘
typ                                        └─────────┘                                  └┘
258  show (units.mk_of_mul_eq_one a b hab : α) ~ᵤ 1, from unit_associated_one
id         └────────────────────┘   └─┘     └┘         └─────────────────┘
src        └────────────────────┘              └┘         └─────────────────┘
typ        └────────────────────┘   └─┘     └┘         └─────────────────┘
259  
260  theorem associated_one_of_associated_mul_one [comm_monoid α] {a b : α} :
id                                                 └─────────┘          
src                                                └─────────┘
typ                                                └─────────┘          
261    a * b ~ᵤ 1 → a ~ᵤ 1
id        └┘     └┘
src         └┘       └┘
typ       └┘     └┘
262  | ⟨u, h⟩ := associated_one_of_mul_eq_one (b * u) $ by simpa [mul_assoc] using h
id              └──────────────────────────┘                   └───────┘        
src              └──────────────────────────┘             └─────┘└───────┘└──────┘ 
typ             └──────────────────────────┘            └─────┘└───────┘└──────┘
doc                                                        └─────┘         └──────┘ 
txt                                                        └─────┘         └──────┘ 
par                                                        └─────┘         └──────┘ 
pid                                                                      └────┘ 
st                                                        └──────────────────────────
263  
src  
typ  
doc  
txt  
par  
pid  
st   
264  lemma associated_mul_mul [comm_monoid α] {a₁ a₂ b₁ b₂ : α} :
id                             └─────────┘                  
src                            └─────────┘
typ                            └─────────┘                  
265    a₁ ~ᵤ b₁ → a₂ ~ᵤ b₂ → (a₁ * a₂) ~ᵤ (b₁ * b₂)
id     └┘ └┘ └┘  └┘ └┘ └┘    └┘  └┘  └┘  └┘  └┘
src       └┘         └┘               └┘     
typ    └┘ └┘ └┘  └┘ └┘ └┘    └┘  └┘  └┘  └┘  └┘
266  | ⟨c₁, h₁⟩ ⟨c₂, h₂⟩ := ⟨c₁ * c₂, by simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]⟩
id      └┘       └┘                                             └───────┘  └──────┘  └───────────┘
src                                     └────┘       └┘       └┘└───────┘└┘└──────┘└┘└───────────┘
typ     └┘       └┘                     └────┘└─────┘└┘└─────┘└┘└───────┘└┘└──────┘└┘└───────────┘
doc                                      └────┘       └┘       └┘         └┘        └┘             
txt                                      └────┘       └┘       └┘         └┘        └┘             
par                                      └────┘       └┘       └┘         └┘        └┘             
pid                                                 └┘       └┘         └┘        └┘             
st                                      └──────────────────────────────────────────────────────────┘
267  
268  theorem associated_of_dvd_dvd [integral_domain α] {a b : α} (hab : a ∣ b) (hba : b ∣ a) : a ~ᵤ b :=
id                                  └─────────────┘                                     └┘ 
src                                 └─────────────┘                                            └┘
typ                                 └─────────────┘                                     └┘ 
269  begin
st   └─────
270    haveI := classical.dec_eq α,
id              └──────────────┘ 
src    └───────┘└──────────────┘
typ    └───────┘└──────────────┘
doc    └───────┘                
txt    └───────┘                
par    └───────┘                
pid         └─┘                
st   ────────────────────────────┘└─
271    rcases hab with ⟨c, rfl⟩,
id            └─┘
src    └─────┘   └────────────┘
typ    └─────┘└─┘└────────────┘
doc    └─────┘   └────────────┘
txt    └─────┘   └────────────┘
par    └─────┘   └────────────┘
pid             └────────────┘
st   ─────────────────────────┘└─
272    rcases hba with ⟨d, a_eq⟩,
id            └─┘
src    └─────┘   └─────────────┘
typ    └─────┘└─┘└─────────────┘
doc    └─────┘   └─────────────┘
txt    └─────┘   └─────────────┘
par    └─────┘   └─────────────┘
pid             └─────────────┘
st   ──────────────────────────┘└─
273    by_cases ha0 : a = 0,
id                     
src    └───────┘   └─┘ └┘
typ    └───────┘   └─┘└┘
doc    └───────┘   └─┘  └┘
txt    └───────┘   └─┘  └┘
par    └───────┘   └─┘  └┘
pid               └─┘  
st   ─────────────────────┘└─
274    { simp [*] at * },
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid          └─┘└──┘
st   ───┘└────────────┘└┘
275    have : a * 1 = a * (c * d),
id                          
src    └─────┘ └─┘       
typ    └─────┘ └─┘    
doc    └─────┘  └─┘       
txt    └─────┘  └─┘       
par    └─────┘  └─┘       
pid    └───┘└┘  └─┘       
st   ───────────────────────────┘└─
276    { simpa [mul_assoc] using a_eq },
id              └───────┘        └──┘
src      └─────┘└───────┘└──────┘    
typ      └─────┘└───────┘└──────┘└──┘
doc      └─────┘         └──────┘    
txt      └─────┘         └──────┘    
par      └─────┘         └──────┘    
pid                    └────┘    
st   ───┘└───────────────────────────┘└┘
277    have : 1 = (c * d), from eq_of_mul_eq_mul_left ha0 this,
id                            └───────────────────┘ └─┘ └──┘
src    └───────┘       └───┘└───────────────────┘   
typ    └───────┘     └───┘└───────────────────┘└─┘└──┘
doc    └───────┘       └───┘                        
txt    └───────┘       └───┘                        
par    └───────┘       └───┘                        
pid    └───┘└──┘       └───┘                        
st   ───────────────────┘└───────────────────────────────────┘└─
278    exact ⟨units.mk_of_mul_eq_one c d (this.symm), by rw [units.mk_of_mul_eq_one, units.val_coe]⟩
id            └────────────────────┘    └───────┘          └────────────────────┘  └───────────┘
src    └────┘ └────────────────────┘   └───────┘└─┘  └──┘└────────────────────┘└┘└───────────┘└┘
typ    └────┘ └────────────────────┘ └───────┘└─┘  └──┘└────────────────────┘└┘└───────────┘└┘
doc    └────┘                                   └─┘  └──┘                      └┘             └┘
txt    └────┘                                   └─┘  └──┘                      └┘             └┘
par    └────┘                                   └─┘  └──┘                      └┘             └┘
pid                                            └─┘  └───┘                      └┘             └┘
st   ──────────────────────────────────────────────────┘└─────────────────────────┘└─────────────┘└┘
279  end
st   └─┘
280  
281  lemma exists_associated_mem_of_dvd_prod [integral_domain α] {p : α}
id                                            └─────────────┘        
src                                           └─────────────┘
typ                                           └─────────────┘        
282    (hp : prime p) {s : multiset α} : (∀ r ∈ s, prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q :=
id           └───┘        └──────┘             └───┘       └───┘         └┘ 
src          └───┘         └──────┘               └───┘          └───┘            └┘
typ          └───┘        └──────┘             └───┘       └───┘         └┘ 
doc          └───┘         └──────┘                └───┘           └───┘
283  multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.not_unit])
id   └───────────────────┘            └┘ └─────────────────┘   └─────────┘
src  └───────────────────┘       └────┘└┘└─────────────────┘└─┘└─────────┘
typ  └───────────────────┘      └────┘└┘└─────────────────┘└─┘└─────────┘
doc                              └────┘                     └─┘           
txt                              └────┘                     └─┘           
par                              └────┘                     └─┘           
pid                                                       └─┘           
st                              └──────────────────────────────────────────┘
284    (λ a s ih hs hps, begin
id          └┘ └┘ └─┘
typ         └┘ └┘ └─┘
st                       └─────
285      rw [multiset.prod_cons] at hps,
id           └────────────────┘
src      └──┘└────────────────┘└──────┘
typ      └──┘└────────────────┘└──────┘
doc      └──┘                  └──────┘
txt      └──┘                  └──────┘
par      └──┘                  └──────┘
pid        └┘                  └─────┘
st   ─────────────────────────┘└─────┘└─
286      cases hp.div_or_div hps with h h,
id             └───────────┘ └─┘
src      └────┘└───────────┘   └───────┘
typ      └────┘└───────────┘└─┘└───────┘
doc      └────┘                └───────┘
txt      └────┘                └───────┘
par      └────┘                └───────┘
pid                           └───────┘
st   ───────────────────────────────────┘└─
287      { use [a, by simp],
id              
src        └───┘ └┘  └──┘
typ        └───┘└┘  └──┘
doc        └───┘ └┘  └──┘
txt        └───┘ └┘  └──┘
par        └───┘ └┘  └──┘
pid           └┘ └┘  └────┘
st   ─────┘└────────┘└───┘└─
288        cases h with u hu,
id               
src        └────┘ └────────┘
typ        └────┘└────────┘
doc        └────┘ └────────┘
txt        └────┘ └────────┘
par        └────┘ └────────┘
pid              └────────┘
st   ──────────────────────┘└─
289        cases ((irreducible_of_prime (hs a (multiset.mem_cons.2
id                 └──────────────────┘  └┘   └───────────────┘
src        └────┘  └──────────────────┘     └───────────────┘└──
typ        └────┘  └──────────────────┘ └┘ └───────────────┘└──
doc        └────┘                                            └──
txt        └────┘                                            └──
par        └────┘                                            └──
pid                                                         └──
st   ──────────────────────────────────────────────────────────────
290          (or.inl rfl)))).2 p u hu).resolve_left hp.not_unit with v hv,
id            └────┘ └─┘         └┘               └─────────┘
src  ───────┘ └────┘└─┘└─────┘    └─────────────┘└─────────┘└────────┘
typ  ───────┘ └────┘└─┘└─────┘└┘└─────────────┘└─────────┘└────────┘
doc  ───────┘          └─────┘    └─────────────┘           └────────┘
txt  ───────┘          └─────┘    └─────────────┘           └────────┘
par  ───────┘          └─────┘    └─────────────┘           └────────┘
pid  ───────┘          └─────┘    └─────────────┘           └────────┘
st   ───────────────────────────────────────────────────────────────────┘└─
291        exact ⟨v, by simp [hu, hv]⟩ },
id                           └┘  └┘
src        └────┘  └┘  └────┘  └┘  └┘
typ        └────┘ └┘  └────┘└┘└┘└┘└┘
doc        └────┘  └┘  └────┘  └┘  └┘
txt        └────┘  └┘  └────┘  └┘  └┘
par        └────┘  └┘  └────┘  └┘  └┘
pid               └┘  └─────┘  └┘  └┘
st   ─────────────────┘└────────────┘└┘└┘
292      { rcases ih (λ r hr, hs _ (multiset.mem_cons.2 (or.inr hr))) h with ⟨q, hq₁, hq₂⟩,
id                └┘          └┘    └───────────────┘    └────┘       
src        └─────┘    └─────┘  └─┘ └───────────────┘└─┘ └────┘  └──┘ └─────────────────┘
typ        └─────┘└┘  └─────┘└┘└─┘ └───────────────┘└─┘ └────┘  └──┘└─────────────────┘
doc        └─────┘    └─────┘  └─┘                  └─┘         └──┘ └─────────────────┘
txt        └─────┘    └─────┘  └─┘                  └─┘         └──┘ └─────────────────┘
par        └─────┘    └─────┘  └─┘                  └─┘         └──┘ └─────────────────┘
pid                  └─────┘  └─┘                  └─┘         └──┘ └─────────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
293        exact ⟨q, multiset.mem_cons.2 (or.inr hq₁), hq₂⟩ }
id                  └───────────────┘    └────┘ └─┘   └─┘
src        └────┘  └┘└───────────────┘└─┘ └────┘   └─┘   └┘
typ        └────┘ └┘└───────────────┘└─┘ └────┘└─┘└─┘└─┘└┘
doc        └────┘  └┘                 └─┘          └─┘   └┘
txt        └────┘  └┘                 └─┘          └─┘   └┘
par        └────┘  └┘                 └─┘          └─┘   └┘
pid               └┘                 └─┘          └─┘   
st   ──────────────────────────────────────────────────────┘└─
294    end)
st   ────┘
295  
296  lemma dvd_iff_dvd_of_rel_left [comm_semiring α] {a b c : α} (h : a ~ᵤ b) : a ∣ c ↔ b ∣ c :=
id                                  └───────────┘                    └┘           
src                                 └───────────┘                       └┘              
typ                                 └───────────┘                    └┘           
297  let ⟨u, hu⟩ := h in hu ▸ mul_unit_dvd_iff.symm
id   └─┘     └┘             └──────────────┘└───┘
src                          └──────────────┘└───┘
typ  └─┘     └┘             └──────────────┘└───┘
298  
299  @[simp] lemma dvd_mul_unit_iff [comm_semiring α] {a b : α} {u : units α} : a ∣ b * u ↔ a ∣ b :=
id                                   └───────────┘                 └───┘             
src                                  └───────────┘                   └───┘                 
typ                                  └───────────┘                 └───┘             
doc    └──┘
300  ⟨λ ⟨d, hd⟩, ⟨d * (u⁻¹ : units α), by simp [(mul_assoc _ _ _).symm, hd.symm]⟩,
id                  └┘   └───┘              └───────┘
src                    └┘   └───┘        └────┘ └───────┘└────────────┘       
typ                 └┘   └───┘       └────┘ └───────┘└────────────┘└─────┘
doc                                       └────┘          └────────────┘       
txt                                       └────┘          └────────────┘       
par                                       └────┘          └────────────┘       
pid                                                     └────────────┘       
st                                       └─────────────────────────────────────┘
301    λ h, dvd.trans h (by simp)⟩
id         └───────┘ 
src         └───────┘       └──┘
typ        └───────┘      └──┘
doc                         └──┘
txt                         └──┘
par                         └──┘
st                         └───┘
302  
303  lemma dvd_iff_dvd_of_rel_right [comm_semiring α] {a b c : α} (h : b ~ᵤ c) : a ∣ b ↔ a ∣ c :=
id                                   └───────────┘                    └┘           
src                                  └───────────┘                       └┘              
typ                                  └───────────┘                    └┘           
304  let ⟨u, hu⟩ := h in hu ▸ dvd_mul_unit_iff.symm
id   └─┘     └┘             └──────────────┘└───┘
src                          └──────────────┘└───┘
typ  └─┘     └┘             └──────────────┘└───┘
305  
306  lemma eq_zero_iff_of_associated [comm_semiring α] {a b : α} (h : a ~ᵤ b) : a = 0 ↔ b = 0 :=
id                                    └───────────┘                  └┘           
src                                   └───────────┘                     └┘              
typ                                   └───────────┘                  └┘           
307  ⟨λ ha, let ⟨u, hu⟩ := h in by simp [hu.symm, ha],
id      └┘  └─┘                                  └┘
src                                └────┘       └┘  
typ     └┘  └─┘                   └────┘└─────┘└┘└┘
doc                                └────┘       └┘  
txt                                └────┘       └┘  
par                                └────┘       └┘  
pid                                           └┘  
st                                └─────────────────┘
308    λ hb, let ⟨u, hu⟩ := h.symm in by simp [hu.symm, hb]⟩
id       └┘  └─┘            └───┘                      └┘
src                          └───┘       └────┘       └┘  
typ      └┘  └─┘            └───┘       └────┘└─────┘└┘└┘
doc                                      └────┘       └┘  
txt                                      └────┘       └┘  
par                                      └────┘       └┘  
pid                                                 └┘  
st                                      └─────────────────┘
309  
310  lemma ne_zero_iff_of_associated [comm_semiring α] {a b : α} (h : a ~ᵤ b) : a ≠ 0 ↔ b ≠ 0 :=
id                                    └───────────┘                  └┘           
src                                   └───────────┘                     └┘              
typ                                   └───────────┘                  └┘           
311  by haveI := classical.dec; exact not_iff_not.2 (eq_zero_iff_of_associated h)
id               └───────────┘        └─────────┘    └───────────────────────┘ 
src     └───────┘└───────────┘  └────┘└─────────┘└─┘ └───────────────────────┘ └─
typ     └───────┘└───────────┘  └────┘└─────────┘└─┘ └───────────────────────┘└─
doc     └───────┘               └────┘           └─┘                           └─
txt     └───────┘               └────┘           └─┘                           └─
par     └───────┘               └────┘           └─┘                           └─
pid          └─┘                               └─┘                           
st     └──────────────────────────────────────────────────────────────────────────
312  
src  
typ  
doc  
txt  
par  
pid  
st   
313  lemma prime_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q) (hp : prime p) : prime q :=
id                              └───────────┘                  └┘         └───┘     └───┘ 
src                             └───────────┘                     └┘          └───┘      └───┘
typ                             └───────────┘                  └┘         └───┘     └───┘ 
doc                                                                           └───┘      └───┘
314  ⟨(ne_zero_iff_of_associated h).1 hp.ne_zero,
id     └───────────────────────┘    └┘└──────┘
src    └───────────────────────┘       └──────┘
typ    └───────────────────────┘    └┘└──────┘
315    let ⟨u, hu⟩ := h in
id     └─┘    └┘     
typ    └─┘    └┘     
316      ⟨λ ⟨v, hv⟩, hp.not_unit ⟨v * u⁻¹, by simp [hv.symm, hu.symm]⟩,
id                 └┘└───────┘      └┘
src                    └───────┘      └┘     └────┘       └┘       
typ                └┘└───────┘      └┘     └────┘└─────┘└┘└─────┘
doc                                           └────┘       └┘       
txt                                           └────┘       └┘       
par                                           └────┘       └┘       
pid                                                      └┘       
st                                           └──────────────────────┘
317        hu ▸ by { simp [mul_unit_dvd_iff], intros a b, exact hp.div_or_div }⟩⟩
id                        └──────────────┘                     └───────────┘
src                 └────┘└──────────────┘  └────────┘  └────┘└───────────┘
typ                 └────┘└──────────────┘  └────────┘  └────┘└───────────┘
doc                  └────┘                  └────────┘  └────┘             
txt                  └────┘                  └────────┘  └────┘             
par                  └────┘                  └────────┘  └────┘             
pid                                              └──┘                    
st                └────────────────────────┘└──────────┘└────────────────────┘└┘
318  
319  lemma prime_iff_of_associated [comm_semiring α] {p q : α}
id                                  └───────────┘          
src                                 └───────────┘
typ                                 └───────────┘          
320    (h : p ~ᵤ q) : prime p ↔ prime q :=
id           └┘     └───┘   └───┘ 
src           └┘      └───┘    └───┘
typ          └┘     └───┘   └───┘ 
doc                   └───┘     └───┘
321  ⟨prime_of_associated h, prime_of_associated h.symm⟩
id    └─────────────────┘   └─────────────────┘ └───┘
src   └─────────────────┘    └─────────────────┘  └───┘
typ   └─────────────────┘   └─────────────────┘ └───┘
322  
323  lemma is_unit_iff_of_associated [monoid α] {a b : α} (h :  a ~ᵤ b) : is_unit a ↔ is_unit b :=
id                                    └────┘                   └┘     └─────┘   └─────┘ 
src                                   └────┘                      └┘      └─────┘    └─────┘
typ                                   └────┘                   └┘     └─────┘   └─────┘ 
doc                                                                       └─────┘     └─────┘
324  ⟨let ⟨u, hu⟩ := h in λ ⟨v, hv⟩, ⟨v * u, by simp [hv, hu.symm]⟩,
id    └─┘                                        └┘
src                                            └────┘  └┘       
typ   └─┘                                  └────┘└┘└┘└─────┘
doc                                             └────┘  └┘       
txt                                             └────┘  └┘       
par                                             └────┘  └┘       
pid                                                   └┘       
st                                             └─────────────────┘
325    let ⟨u, hu⟩ := h.symm in λ ⟨v, hv⟩, ⟨v * u, by simp [hv, hu.symm]⟩⟩
id     └─┘           └───┘                             └┘
src                    └───┘                         └────┘  └┘       
typ    └─┘           └───┘                       └────┘└┘└┘└─────┘
doc                                                   └────┘  └┘       
txt                                                   └────┘  └┘       
par                                                   └────┘  └┘       
pid                                                         └┘       
st                                                   └─────────────────┘
326  
327  lemma irreducible_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q)
id                                    └───────────┘                  └┘ 
src                                   └───────────┘                     └┘
typ                                   └───────────┘                  └┘ 
328    (hp : irreducible p) : irreducible q :=
id           └─────────┘     └─────────┘ 
src          └─────────┘      └─────────┘
typ          └─────────┘     └─────────┘ 
doc          └─────────┘      └─────────┘
329  ⟨mt (is_unit_iff_of_associated h).2 hp.1,
id    └┘  └───────────────────────┘    └┘
src   └┘  └───────────────────────┘       
typ   └┘  └───────────────────────┘    └┘
330    let ⟨u, hu⟩ := h in λ a b hab,
id     └─┘                   └─┘
typ    └─┘                   └─┘
331    have hpab : p = a * (b * (u⁻¹ : units α)),
id                          └┘   └───┘ 
src                            └┘   └───┘
typ                         └┘   └───┘ 
332      from calc p = (p * u) * (u ⁻¹ : units α) : by simp
id                              └┘   └───┘ 
src                               └┘   └───┘         └────
typ                             └┘   └───┘        └────
doc                                                    └────
txt                                                    └────
par                                                    └────
pid                                                        
st                                                    └─────
333        ... = _ : by rw hu; simp [hab, mul_assoc],
id                         └┘        └─┘  └───────┘
src  ─────┘             └─┘    └────┘   └┘└───────┘
typ  ─────┘             └─┘└┘  └────┘└─┘└┘└───────┘
doc  ─────┘             └─┘    └────┘   └┘         
txt  ─────┘             └─┘    └────┘   └┘         
par  ─────┘             └─┘    └────┘   └┘         
pid  ─────┘                          └┘         
st   ─────┘            └───────────────────────────┘
334    (hp.2 _ _ hpab).elim or.inl (λ ⟨v, hv⟩, or.inr ⟨v * u, by simp [hv.symm]⟩)⟩
id      └┘      └──┘ └──┘  └────┘           └────┘    
src                  └──┘  └────┘             └────┘           └────┘       
typ     └┘      └──┘ └──┘  └────┘           └────┘           └────┘└─────┘
doc                                                              └────┘       
txt                                                              └────┘       
par                                                              └────┘       
pid                                                                         
st                                                              └─────────────┘
335  
336  lemma irreducible_iff_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q) :
id                                        └───────────┘                  └┘ 
src                                       └───────────┘                     └┘
typ                                       └───────────┘                  └┘ 
337    irreducible p ↔ irreducible q :=
id     └─────────┘   └─────────┘ 
src    └─────────┘    └─────────┘
typ    └─────────┘   └─────────┘ 
doc    └─────────┘     └─────────┘
338  ⟨irreducible_of_associated h, irreducible_of_associated h.symm⟩
id    └───────────────────────┘   └───────────────────────┘ └───┘
src   └───────────────────────┘    └───────────────────────┘  └───┘
typ   └───────────────────────┘   └───────────────────────┘ └───┘
339  
340  lemma associated_mul_left_cancel [integral_domain α] {a b c d : α}
id                                     └─────────────┘              
src                                    └─────────────┘
typ                                    └─────────────┘              
341  (h : a * b ~ᵤ c * d) (h₁ : a ~ᵤ c) (ha : a ≠ 0) : b ~ᵤ d :=
id           └┘            └┘                 └┘ 
src            └┘               └┘                    └┘
typ          └┘            └┘                 └┘ 
342  let ⟨u, hu⟩ := h in let ⟨v, hv⟩ := associated.symm h₁ in
id   └─┘               └─┘           └─────────────┘ └┘
src                                     └─────────────┘
typ  └─┘               └─┘           └─────────────┘ └┘
343  ⟨u * (v : units α), (domain.mul_left_inj ha).1
id            └───┘     └─────────────────┘ └┘ 
src           └───┘      └─────────────────┘    
typ           └───┘     └─────────────────┘ └┘ 
doc                       └─────────────────┘
344    begin
st     └─────
345      rw [← hv, mul_assoc c (v : α) d, mul_left_comm c, ← hu],
id             └┘  └───────┘          └───────────┘     └┘
src      └────┘  └┘└───────┘   └─┘ └┘ └┘└───────────┘ └──┘  
typ      └────┘└┘└┘└───────┘ └─┘└┘└┘└───────────┘└──┘└┘
doc      └────┘  └┘            └─┘ └┘ └┘              └──┘  
txt      └────┘  └┘            └─┘ └┘ └┘              └──┘  
par      └────┘  └┘            └─┘ └┘ └┘              └──┘  
pid        └──┘  └┘            └─┘ └┘ └┘              └──┘  
st   ───────────┘└─────────────────────┘└───────────────┘└────┘└──
346      simp [hv.symm, mul_assoc, mul_comm, mul_left_comm]
id                      └───────┘  └──────┘  └───────────┘
src      └────┘       └┘└───────┘└┘└──────┘└┘└───────────┘└─
typ      └────┘└─────┘└┘└───────┘└┘└──────┘└┘└───────────┘└─
doc      └────┘       └┘         └┘        └┘             └─
txt      └────┘       └┘         └┘        └┘             └─
par      └────┘       └┘         └┘        └┘             └─
pid                 └┘         └┘        └┘             
st   ───────────────────────────────────────────────────────
347    end⟩
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
348  
349  lemma associated_mul_right_cancel [integral_domain α] {a b c d : α} :
id                                      └─────────────┘              
src                                     └─────────────┘
typ                                     └─────────────┘              
350    a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c :=
id        └┘       └┘           └┘ 
src         └┘          └┘              └┘
typ       └┘       └┘           └┘ 
351  by rw [mul_comm a, mul_comm c]; exact associated_mul_left_cancel
id          └──────┘   └──────┘          └────────────────────────┘
src     └──┘└──────┘ └┘└──────┘   └────┘└────────────────────────┘
typ     └──┘└──────┘└┘└──────┘  └────┘└────────────────────────┘
doc     └──┘         └┘           └────┘                          
txt     └──┘         └┘           └────┘                          
par     └──┘         └┘           └────┘                          
pid       └┘         └┘                                          
st     └─────────────┘└──────────┘└──────────────────────────────────
352  
src  
typ  
doc  
txt  
par  
pid  
st   
353  def associates (α : Type*) [monoid α] : Type* :=
id                               └────┘ 
src                              └────┘
typ                              └────┘ 
354  quotient (associated.setoid α)
id   └──────┘  └───────────────┘ 
src  └──────┘  └───────────────┘
typ  └──────┘  └───────────────┘ 
355  
356  namespace associates
357  open associated
358  
359  protected def mk {α : Type*} [monoid α] (a : α) : associates α :=
id                                 └────┘            └────────┘ 
src                                └────┘              └────────┘
typ                                └────┘            └────────┘ 
360  ⟦ a ⟧
id     
src     
typ    
361  
362  instance [monoid α] : inhabited (associates α) := ⟨⟦1⟧⟩
id             └────┘     └───────┘  └────────┘        
src            └────┘      └───────┘  └────────┘         
typ            └────┘     └───────┘  └────────┘        
363  
364  theorem mk_eq_mk_iff_associated [monoid α] {a b : α} :
id                                    └────┘          
src                                   └────┘
typ                                   └────┘          
365    associates.mk a = associates.mk b ↔ a ~ᵤ b :=
id     └───────────┘   └───────────┘    └┘ 
src    └───────────┘    └───────────┘      └┘
typ    └───────────┘   └───────────┘    └┘ 
366  iff.intro quotient.exact quot.sound
id   └───────┘ └────────────┘ └────────┘
src  └───────┘ └────────────┘ └────────┘
typ  └───────┘ └────────────┘ └────────┘
367  
368  theorem quotient_mk_eq_mk [monoid α] (a : α) : ⟦ a ⟧ = associates.mk a := rfl
id                              └────┘                └───────────┘     └─┘
src                             └────┘                   └───────────┘      └─┘
typ                             └────┘                └───────────┘     └─┘
369  
370  theorem quot_mk_eq_mk [monoid α] (a : α) : quot.mk setoid.r a = associates.mk a := rfl
id                          └────┘            └─────┘ └──────┘   └───────────┘     └─┘
src                         └────┘                      └──────┘    └───────────┘      └─┘
typ                         └────┘            └─────┘ └──────┘   └───────────┘     └─┘
371  
372  theorem forall_associated [monoid α] {p : associates α → Prop} :
id                              └────┘        └────────┘ 
src                             └────┘         └────────┘
typ                             └────┘        └────────┘ 
373    (∀a, p a) ↔ (∀a, p (associates.mk a)) :=
id                   └───────────┘ 
src                       └───────────┘
typ                  └───────────┘ 
374  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
375    (assume h a, h _)
id                
typ               
376    (assume h a, quotient.induction_on a h)
id                └───────────────────┘  
src                 └───────────────────┘
typ               └───────────────────┘  
377  
378  instance [monoid α] : has_one (associates α) := ⟨⟦ 1 ⟧⟩
id             └────┘     └─────┘  └────────┘          
src            └────┘      └─────┘  └────────┘           
typ            └────┘     └─────┘  └────────┘          
379  
380  theorem one_eq_mk_one [monoid α] : (1 : associates α) = associates.mk 1 := rfl
id                          └────┘          └────────┘    └───────────┘      └─┘
src                         └────┘           └────────┘     └───────────┘      └─┘
typ                         └────┘          └────────┘    └───────────┘      └─┘
381  
382  instance [monoid α] : has_bot (associates α) := ⟨1⟩
id             └────┘     └─────┘  └────────┘ 
src            └────┘      └─────┘  └────────┘
typ            └────┘     └─────┘  └────────┘ 
doc                        └─────┘
383  
384  section comm_monoid
385  variable [comm_monoid α]
id             └─────────┘
src            └─────────┘
typ            └─────────┘
386  
387  instance : has_mul (associates α) :=
id              └─────┘  └────────┘ 
src             └─────┘  └────────┘
typ             └─────┘  └────────┘ 
388  ⟨λa' b', quotient.lift_on₂ a' b' (λa b, ⟦ a * b ⟧) $
id     └┘ └┘  └───────────────┘ └┘ └┘          
src           └───────────────┘                    
typ    └┘ └┘  └───────────────┘ └┘ └┘          
389    assume a₁ a₂ b₁ b₂ ⟨c₁, h₁⟩ ⟨c₂, h₂⟩,
id            └┘ └┘ └┘ └┘ └┘      └┘
typ           └┘ └┘ └┘ └┘ └┘      └┘
390    quotient.sound $ ⟨c₁ * c₂, by simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]⟩⟩
id     └────────────┘                                       └───────┘  └──────┘  └───────────┘
src    └────────────┘               └────┘       └┘       └┘└───────┘└┘└──────┘└┘└───────────┘
typ    └────────────┘               └────┘└─────┘└┘└─────┘└┘└───────┘└┘└──────┘└┘└───────────┘
doc                                  └────┘       └┘       └┘         └┘        └┘             
txt                                  └────┘       └┘       └┘         └┘        └┘             
par                                  └────┘       └┘       └┘         └┘        └┘             
pid                                             └┘       └┘         └┘        └┘             
st                                  └──────────────────────────────────────────────────────────┘
391  
392  theorem mk_mul_mk {x y : α} : associates.mk x * associates.mk y = associates.mk (x * y) :=
id                                └───────────┘   └───────────┘   └───────────┘    
src                                └───────────┘    └───────────┘    └───────────┘    
typ                               └───────────┘   └───────────┘   └───────────┘    
393  rfl
id   └─┘
src  └─┘
typ  └─┘
394  
395  instance : comm_monoid (associates α) :=
id              └─────────┘  └────────┘ 
src             └─────────┘  └────────┘
typ             └─────────┘  └────────┘ 
396  { one       := 1,
397    mul       := (*),
id                  
src                 
typ                 
398    mul_one   := assume a', quotient.induction_on a' $
id                         └┘  └───────────────────┘ └┘
src                            └───────────────────┘
typ                        └┘  └───────────────────┘ └┘
399      assume a, show ⟦a * 1⟧ = ⟦ a ⟧, by simp,
id                            
src                                   └──┘
typ                                └──┘
doc                                         └──┘
txt                                         └──┘
par                                         └──┘
st                                         └───┘
400    one_mul   := assume a', quotient.induction_on a' $
id                         └┘  └───────────────────┘ └┘
src                            └───────────────────┘
typ                        └┘  └───────────────────┘ └┘
401      assume a, show ⟦1 * a⟧ = ⟦ a ⟧, by simp,
id                            
src                                   └──┘
typ                                └──┘
doc                                         └──┘
txt                                         └──┘
par                                         └──┘
st                                         └───┘
402    mul_assoc := assume a' b' c', quotient.induction_on₃ a' b' c' $
id                         └┘ └┘ └┘  └────────────────────┘ └┘ └┘ └┘
src                                  └────────────────────┘
typ                        └┘ └┘ └┘  └────────────────────┘ └┘ └┘ └┘
403      assume a b c, show ⟦a * b * c⟧ = ⟦a * (b * c)⟧, by rw [mul_assoc],
id                                            └───────┘
src                                                └──┘└───────┘
typ                                       └──┘└───────┘
doc                                                         └──┘         
txt                                                         └──┘         
par                                                         └──┘         
pid                                                           └┘         
st                                                         └────────────┘
404    mul_comm  := assume a' b', quotient.induction_on₂ a' b' $
id                         └┘ └┘  └────────────────────┘ └┘ └┘
src                               └────────────────────┘
typ                        └┘ └┘  └────────────────────┘ └┘ └┘
405      assume a b, show ⟦a * b⟧ = ⟦b * a⟧, by rw [mul_comm] }
id                                     └──────┘
src                                      └──┘└──────┘└┘
typ                                └──┘└──────┘└┘
doc                                             └──┘        └┘
txt                                             └──┘        └┘
par                                             └──┘        └┘
pid                                               └┘        
st                                             └───────────┘
406  
407  instance : preorder (associates α) :=
id              └──────┘  └────────┘ 
src             └──────┘  └────────┘
typ             └──────┘  └────────┘ 
408  { le := λa b, ∃c, a * c = b,
id                   
src                      
typ                  
409    le_refl := assume a, ⟨1, by simp⟩,
id                       
src                                └──┘
typ                               └──┘
doc                                └──┘
txt                                └──┘
par                                └──┘
st                                └───┘
410    le_trans := assume a b c ⟨f₁, h₁⟩ ⟨f₂, h₂⟩, ⟨f₁ * f₂, h₂ ▸ h₁ ▸ (mul_assoc _ _ _).symm⟩}
id                           └┘  └┘  └┘  └┘                     └───────┘       └──┘
src                                                                  └───────┘       └──┘
typ                          └┘  └┘  └┘  └┘                     └───────┘       └──┘
411  
412  instance : has_dvd (associates α) := ⟨(≤)⟩
id              └─────┘  └────────┘       
src             └─────┘  └────────┘        
typ             └─────┘  └────────┘       
413  
414  @[simp] lemma mk_one : associates.mk (1 : α) = 1 := rfl
id                          └───────────┘              └─┘
src                         └───────────┘               └─┘
typ                         └───────────┘              └─┘
doc    └──┘
415  
416  lemma mk_pow (a : α) (n : ℕ) : associates.mk (a ^ n) = (associates.mk a) ^ n :=
id                                └───────────┘        └───────────┘    
src                                └───────────┘          └───────────┘    
typ                               └───────────┘        └───────────┘    
417  by induction n; simp [*, pow_succ, associates.mk_mul_mk.symm]
id                           └──────┘
src     └────────┘   └───────┘└──────┘└┘                         └─
typ     └────────┘  └───────┘└──────┘└┘└───────────────────────┘└─
doc     └────────┘   └───────┘        └┘                         └─
txt     └────────┘   └───────┘        └┘                         └─
par     └────────┘   └───────┘        └┘                         └─
pid                     └──┘        └┘                         
st     └───────────────────────────────────────────────────────────
418  
src  
typ  
doc  
txt  
par  
pid  
st   
419  lemma dvd_eq_le : ((∣) : associates α → associates α → Prop) = (≤) := rfl
id                           └────────┘    └────────┘                 └─┘
src                          └────────┘     └────────┘                  └─┘
typ                          └────────┘    └────────┘                 └─┘
420  
421  theorem prod_mk {p : multiset α} : (p.map associates.mk).prod = associates.mk p.prod :=
id                        └──────┘      └──┘ └───────────┘ └──┘   └───────────┘ └───┘
src                       └──────┘        └──┘ └───────────┘ └──┘   └───────────┘  └───┘
typ                       └──────┘      └──┘ └───────────┘ └──┘   └───────────┘ └───┘
doc                       └──────┘        └──┘               └──┘                   └───┘
422  multiset.induction_on p (by simp; refl) $ assume a s ih, by simp [ih]; refl
id   └───────────────────┘                             └┘           └┘
src  └───────────────────┘       └──┘  └──┘                      └────┘    └────
typ  └───────────────────┘      └──┘  └──┘             └┘     └────┘└┘  └────
doc                              └──┘  └──┘                      └────┘    └────
txt                              └──┘  └──┘                      └────┘    └────
par                              └──┘  └──┘                      └────┘    └────
pid                                                                          
st                              └─────────┘                     └────────────────
423  
src  
typ  
doc  
txt  
par  
pid  
st   
424  theorem rel_associated_iff_map_eq_map {p q : multiset α} :
id                                                └──────┘ 
src                                               └──────┘
typ                                               └──────┘ 
doc                                               └──────┘
425    multiset.rel associated p q ↔ p.map associates.mk = q.map associates.mk :=
id     └──────────┘ └────────┘    └──┘ └───────────┘  └──┘ └───────────┘
src    └──────────┘ └────────┘       └──┘ └───────────┘   └──┘ └───────────┘
typ    └──────────┘ └────────┘    └──┘ └───────────┘  └──┘ └───────────┘
doc    └──────────┘                   └──┘                  └──┘
426  by rw [← multiset.rel_eq];
id            └─────────────┘
src     └────┘└─────────────┘
typ     └────┘└─────────────┘
doc     └────┘               
txt     └────┘               
par     └────┘               
pid       └──┘               
st     └────────────────────┘└─
427    simp [multiset.rel_map_left, multiset.rel_map_right, mk_eq_mk_iff_associated]
id           └───────────────────┘  └────────────────────┘  └─────────────────────┘
src    └────┘└───────────────────┘└┘└────────────────────┘└┘└─────────────────────┘└─
typ    └────┘└───────────────────┘└┘└────────────────────┘└┘└─────────────────────┘└─
doc    └────┘                     └┘                      └┘                       └─
txt    └────┘                     └┘                      └┘                       └─
par    └────┘                     └┘                      └┘                       └─
pid                             └┘                      └┘                       
st   ────────────────────────────────────────────────────────────────────────────────
428  
src  
typ  
doc  
txt  
par  
pid  
st   
429  theorem mul_eq_one_iff {x y : associates α} : x * y = 1 ↔ (x = 1 ∧ y = 1) :=
id                                 └────────┘                   
src                                └────────┘                        
typ                                └────────┘                   
430  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
431    (quotient.induction_on₂ x y $ assume a b h,
id      └────────────────────┘              
src     └────────────────────┘
typ     └────────────────────┘              
432      have a * b ~ᵤ 1, from quotient.exact h,
id               └┘         └────────────┘ 
src                └┘         └────────────┘
typ              └┘         └────────────┘ 
433      ⟨quotient.sound $ associated_one_of_associated_mul_one this,
id        └────────────┘   └──────────────────────────────────┘ └──┘
src       └────────────┘   └──────────────────────────────────┘
typ       └────────────┘   └──────────────────────────────────┘ └──┘
434        quotient.sound $ associated_one_of_associated_mul_one $ by rwa [mul_comm] at this⟩)
id         └────────────┘   └──────────────────────────────────┘           └──────┘
src        └────────────┘   └──────────────────────────────────┘      └───┘└──────┘└───────┘
typ        └────────────┘   └──────────────────────────────────┘      └───┘└──────┘└───────┘
doc                                                                   └───┘        └───────┘
txt                                                                   └───┘        └───────┘
par                                                                   └───┘        └───────┘
pid                                                                      └┘        └──────┘
st                                                                   └────────────┘└──────┘
435    (by simp {contextual := tt})
id                             └┘
src        └───┘ └────────────┘└┘
typ        └───┘ └────────────┘└┘
doc        └───┘ └────────────┘  
txt        └───┘ └────────────┘  
par        └───┘ └────────────┘  
pid             └────────────┘  
st        └──────────────────────┘
436  
437  theorem prod_eq_one_iff {p : multiset (associates α)} :
id                                └──────┘  └────────┘ 
src                               └──────┘  └────────┘
typ                               └──────┘  └────────┘ 
doc                               └──────┘
438    p.prod = 1 ↔ (∀a ∈ p, (a:associates α) = 1) :=
id     └───┘              └────────┘   
src     └───┘                 └────────┘    
typ    └───┘              └────────┘   
doc     └───┘
439  multiset.induction_on p
id   └───────────────────┘ 
src  └───────────────────┘
typ  └───────────────────┘ 
440    (by simp)
src        └──┘
typ        └──┘
doc        └──┘
txt        └──┘
par        └──┘
st        └───┘
441    (by simp [mul_eq_one_iff, or_imp_distrib, forall_and_distrib] {contextual := tt})
id               └────────────┘  └────────────┘  └────────────────┘                 └┘
src        └────┘└────────────┘└┘└────────────┘└┘└────────────────┘└┘ └────────────┘└┘
typ        └────┘└────────────┘└┘└────────────┘└┘└────────────────┘└┘ └────────────┘└┘
doc        └────┘              └┘              └┘                  └┘ └────────────┘  
txt        └────┘              └┘              └┘                  └┘ └────────────┘  
par        └────┘              └┘              └┘                  └┘ └────────────┘  
pid                          └┘              └┘                   └────────────┘  
st        └───────────────────────────────────────────────────────────────────────────┘
442  
443  theorem coe_unit_eq_one : ∀u:units (associates α), (u : associates α) = 1
id                               └───┘  └────────┘        └────────┘   
src                               └───┘  └────────┘          └────────┘    
typ                              └───┘  └────────┘        └────────┘   
444  | ⟨u, v, huv, hvu⟩ := by rw [mul_eq_one_iff] at huv; exact huv.1
id                                └────────────┘                └─┘
src                           └──┘└────────────┘└──────┘  └────┘   └──
typ                           └──┘└────────────┘└──────┘  └────┘└─┘└──
doc                           └──┘              └──────┘  └────┘   └──
txt                           └──┘              └──────┘  └────┘   └──
par                           └──┘              └──────┘  └────┘   └──
pid                             └┘              └─────┘          └──
st                           └─────────────────┘└────────────────────
445  
src  
typ  
doc  
txt  
par  
pid  
st   
446  theorem is_unit_iff_eq_one (a : associates α) : is_unit a ↔ a = 1 :=
id                                   └────────┘     └─────┘    
src                                  └────────┘      └─────┘      
typ                                  └────────┘     └─────┘    
doc                                                  └─────┘
447  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
448    (assume ⟨u, h⟩, h.symm ▸ coe_unit_eq_one _)
id                    └───┘  └─────────────┘
src                     └───┘  └─────────────┘
typ                   └───┘  └─────────────┘
449    (assume h, h.symm ▸ is_unit_one)
id               └───┘  └─────────┘
src                └───┘  └─────────┘
typ              └───┘  └─────────┘
450  
451  theorem is_unit_mk {a : α} : is_unit (associates.mk a) ↔ is_unit a :=
id                               └─────┘  └───────────┘    └─────┘ 
src                               └─────┘  └───────────┘     └─────┘
typ                              └─────┘  └───────────┘    └─────┘ 
doc                               └─────┘                     └─────┘
452  calc is_unit (associates.mk a) ↔ a ~ᵤ 1 :
id        └─────┘  └───────────┘      └┘
src       └─────┘  └───────────┘        └┘
typ       └─────┘  └───────────┘      └┘
doc       └─────┘
453      by rw [is_unit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]
id              └────────────────┘  └───────────┘  └─────────────────────┘
src         └──┘└────────────────┘└┘└───────────┘└┘└─────────────────────┘└─
typ         └──┘└────────────────┘└┘└───────────┘└┘└─────────────────────┘└─
doc         └──┘                  └┘             └┘                       └─
txt         └──┘                  └┘             └┘                       └─
par         └──┘                  └┘             └┘                       └─
pid           └┘                  └┘             └┘                       
st         └─────────────────────┘└─────────────┘└───────────────────────┘
454    ... ↔ is_unit a : associated_one_iff_is_unit
id           └─────┘    └────────────────────────┘
src  ─┘      └─────┘     └────────────────────────┘
typ  ─┘      └─────┘    └────────────────────────┘
doc  ─┘      └─────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
455  
456  section order
457  
458  theorem mul_mono {a b c d : associates α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
id                               └────────┘                     
src                              └────────┘                        
typ                              └────────┘                     
459    a * c ≤ b * d :=
id           
src            
typ          
460  let ⟨x, hx⟩ := h₁, ⟨y, hy⟩ := h₂ in
id   └─┘           └┘            └┘
typ  └─┘           └┘            └┘
461  ⟨x * y, by simp [hx.symm, hy.symm, mul_comm, mul_assoc, mul_left_comm]⟩
id                                     └──────┘  └───────┘  └───────────┘
src            └────┘       └┘       └┘└──────┘└┘└───────┘└┘└───────────┘
typ            └────┘└─────┘└┘└─────┘└┘└──────┘└┘└───────┘└┘└───────────┘
doc             └────┘       └┘       └┘        └┘         └┘             
txt             └────┘       └┘       └┘        └┘         └┘             
par             └────┘       └┘       └┘        └┘         └┘             
pid                        └┘       └┘        └┘         └┘             
st             └──────────────────────────────────────────────────────────┘
462  
463  theorem one_le {a : associates α} : 1 ≤ a :=
id                       └────────┘        
src                      └────────┘        
typ                      └────────┘        
464  ⟨a, one_mul a⟩
id      └─────┘ 
src      └─────┘
typ     └─────┘ 
465  
466  theorem prod_le_prod {p q : multiset (associates α)} (h : p ≤ q) : p.prod ≤ q.prod :=
id                               └──────┘  └────────┘               └───┘  └───┘
src                              └──────┘  └────────┘                   └───┘   └───┘
typ                              └──────┘  └────────┘               └───┘  └───┘
doc                              └──────┘                                └───┘    └───┘
467  begin
st   └─────
468    haveI := classical.dec_eq (associates α),
id              └──────────────┘  └────────┘ 
src    └───────┘└──────────────┘ └────────┘ 
typ    └───────┘└──────────────┘ └────────┘
doc    └───────┘                            
txt    └───────┘                            
par    └───────┘                            
pid         └─┘                            
st   ─────────────────────────────────────────┘└─
469    haveI := classical.dec_eq α,
id              └──────────────┘ 
src    └───────┘└──────────────┘
typ    └───────┘└──────────────┘
doc    └───────┘                
txt    └───────┘                
par    └───────┘                
pid         └─┘                
st   ────────────────────────────┘└─
470    suffices : p.prod ≤ (p + (q - p)).prod, { rwa [multiset.add_sub_of_le h] at this },
id                └────┘                         └────────────────────┘ 
src    └─────────┘└────┘     └─────┘    └───┘└────────────────────┘ └────────┘
typ    └─────────┘└────┘   └─────┘    └───┘└────────────────────┘└────────┘
doc    └─────────┘└────┘        └─────┘    └───┘                       └────────┘
txt    └─────────┘              └─────┘    └───┘                       └────────┘
par    └─────────┘              └─────┘    └───┘                       └────────┘
pid    └───────┘└┘              └────┘       └┘                       └──────┘
st   ───────────────────────────────────────┘└──┘└───────────────────────────┘└───────┘└┘
471    suffices : p.prod * 1 ≤ p.prod * (q - p).prod, { simpa },
id                            └────┘       
src    └─────────┘      └─┘ └────┘     └────┘    └────┘
typ    └─────────┘      └─┘ └────┘   └────┘    └────┘
doc    └─────────┘       └─┘ └────┘     └────┘    └────┘
txt    └─────────┘       └─┘            └────┘    └────┘
par    └─────────┘       └─┘            └────┘    └────┘
pid    └───────┘└┘       └─┘            └───┘         
st   ──────────────────────────────────────────────┘└──┘└────┘└┘
472    exact mul_mono (le_refl p.prod) one_le
id           └──────┘  └─────┘ └────┘  └────┘
src    └────┘└──────┘ └─────┘└────┘└┘└────┘
typ    └────┘└──────┘ └─────┘└────┘└┘└────┘
doc    └────┘                └────┘└┘      
txt    └────┘                      └┘      
par    └────┘                      └┘      
pid                               └┘      
st   ────────────────────────────────────────┘
473  end
st   └─┘
474  
475  theorem le_mul_right {a b : associates α} : a ≤ a * b := ⟨b, rfl⟩
id                               └────────┘                └─┘
src                              └────────┘                     └─┘
typ                              └────────┘                └─┘
476  
477  theorem le_mul_left {a b : associates α} : a ≤ b * a :=
id                              └────────┘         
src                             └────────┘           
typ                             └────────┘         
478  by rw [mul_comm]; exact le_mul_right
id          └──────┘         └──────────┘
src     └──┘└──────┘  └────┘└──────────┘
typ     └──┘└──────┘  └────┘└──────────┘
doc     └──┘          └────┘            
txt     └──┘          └────┘            
par     └──┘          └────┘            
pid       └┘                           
st     └───────────┘└────────────────────
479  
src  
typ  
doc  
txt  
par  
pid  
st   
480  end order
481  
482  end comm_monoid
483  
484  instance [has_zero α] [monoid α] : has_zero (associates α) := ⟨⟦ 0 ⟧⟩
id             └──────┘    └────┘     └──────┘  └────────┘          
src            └──────┘     └────┘      └──────┘  └────────┘           
typ            └──────┘    └────┘     └──────┘  └────────┘          
485  instance [has_zero α] [monoid α] : has_top (associates α) := ⟨0⟩
id             └──────┘    └────┘     └─────┘  └────────┘ 
src            └──────┘     └────┘      └─────┘  └────────┘
typ            └──────┘    └────┘     └─────┘  └────────┘ 
doc                                     └─────┘
486  
487  section comm_semiring
488  variables [comm_semiring α]
id              └───────────┘
src             └───────────┘
typ             └───────────┘
489  
490  @[simp] theorem mk_zero_eq (a : α) : associates.mk a = 0 ↔ a = 0 :=
id                                       └───────────┘       
src                                       └───────────┘         
typ                                      └───────────┘       
doc    └──┘
491  ⟨assume h, (associated_zero_iff_eq_zero a).1 $ quotient.exact h, assume h, h.symm ▸ rfl⟩
id              └─────────────────────────┘      └────────────┘            └───┘  └─┘
src              └─────────────────────────┘       └────────────┘               └───┘  └─┘
typ             └─────────────────────────┘      └────────────┘            └───┘  └─┘
492  
493  @[simp] theorem mul_zero : ∀(a : associates α), a * 0 = 0 :=
id                                    └────────┘        
src                                   └────────┘          
typ                                   └────────┘        
doc    └──┘
494  by rintros ⟨a⟩; show associates.mk (a * 0) = associates.mk 0; rw [mul_zero]
id                                             └───────────┘        └──────┘
src     └─────────┘  └───┘               └──┘└───────────┘└┘  └──┘└──────┘└─
typ     └─────────┘  └───┘              └──┘└───────────┘└┘  └──┘└──────┘└─
doc     └─────────┘  └───┘                └──┘              └┘  └──┘        └─
txt     └─────────┘  └───┘                └──┘              └┘  └──┘        └─
par     └─────────┘  └───┘                └──┘              └┘  └──┘        └─
pid            └──┘  └───┘                └──┘                  └┘        
st     └──────────────────────────────────────────────────────────────┘└──────┘
495  
src  
typ  
doc  
txt  
par  
pid  
st   
496  @[simp] protected theorem zero_mul : ∀(a : associates α), 0 * a = 0 :=
id                                              └────────┘        
src                                             └────────┘          
typ                                             └────────┘        
doc    └──┘
497  by rintros ⟨a⟩; show associates.mk (0 * a) = associates.mk 0; rw [zero_mul]
id                                             └───────────┘        └──────┘
src     └─────────┘  └───┘              └┘ └┘└───────────┘└┘  └──┘└──────┘└─
typ     └─────────┘  └───┘              └┘└┘└───────────┘└┘  └──┘└──────┘└─
doc     └─────────┘  └───┘              └┘  └┘              └┘  └──┘        └─
txt     └─────────┘  └───┘              └┘  └┘              └┘  └──┘        └─
par     └─────────┘  └───┘              └┘  └┘              └┘  └──┘        └─
pid            └──┘  └───┘              └┘  └┘                  └┘        
st     └──────────────────────────────────────────────────────────────┘└──────┘
498  
src  
typ  
doc  
txt  
par  
pid  
st   
499  theorem mk_eq_zero_iff_eq_zero {a : α} : associates.mk a = 0 ↔ a = 0 :=
id                                           └───────────┘       
src                                           └───────────┘         
typ                                          └───────────┘       
500  calc associates.mk a = 0 ↔ (a ~ᵤ 0) :  mk_eq_mk_iff_associated
id        └───────────┘         └┘       └─────────────────────┘
src       └───────────┘           └┘       └─────────────────────┘
typ       └───────────┘         └┘       └─────────────────────┘
501    ... ↔ a = 0 : associated_zero_iff_eq_zero a
id                 └─────────────────────────┘ 
src                 └─────────────────────────┘
typ                └─────────────────────────┘ 
502  
503  theorem dvd_of_mk_le_mk {a b : α} : associates.mk a ≤ associates.mk b → a ∣ b
id                                      └───────────┘   └───────────┘     
src                                      └───────────┘    └───────────┘       
typ                                     └───────────┘   └───────────┘     
504  | ⟨c', hc'⟩ := (quotient.induction_on c' $ assume c hc,
id      └┘  └─┘      └───────────────────┘              └┘
src                  └───────────────────┘
typ     └┘  └─┘      └───────────────────┘              └┘
505      let ⟨d, hd⟩ := (quotient.exact hc).symm in
id       └─┘            └────────────┘ └┘ └──┘
src                      └────────────┘    └──┘
typ      └─┘            └────────────┘ └┘ └──┘
506      ⟨(↑d⁻¹) * c,
id          └┘   
src         └┘  
typ         └┘   
507        calc b = (a * c) * ↑d⁻¹ : by rw [← hd, mul_assoc, units.mul_inv, mul_one]
id                        └┘            └┘  └───────┘  └───────────┘  └─────┘
src                          └┘      └────┘  └┘└───────┘└┘└───────────┘└┘└─────┘└─
typ                       └┘      └────┘└┘└┘└───────┘└┘└───────────┘└┘└─────┘└─
doc                                     └────┘  └┘         └┘             └┘       └─
txt                                     └────┘  └┘         └┘             └┘       └─
par                                     └────┘  └┘         └┘             └┘       └─
pid                                       └──┘  └┘         └┘             └┘       
st                                     └───────┘└─────────┘└─────────────┘└───────┘
508          ... = a * (↑d⁻¹ * c) : by ac_refl⟩) hc'
id                     └┘  
src  ───────┘           └┘          └─────┘
typ  ───────┘          └┘         └─────┘
doc  ───────┘                          └─────┘
txt  ───────┘                          └─────┘
par  ───────┘                          └─────┘
pid  ───────┘
st   ───────┘                         └──────┘
509  
510  theorem mk_le_mk_of_dvd {a b : α} : a ∣ b → associates.mk a ≤ associates.mk b :=
id                                           └───────────┘   └───────────┘ 
src                                             └───────────┘    └───────────┘
typ                                          └───────────┘   └───────────┘ 
511  assume ⟨c, hc⟩, ⟨associates.mk c, by simp [hc]; refl⟩
id                  └───────────┘             └┘
src                   └───────────┘       └────┘    └──┘
typ                 └───────────┘       └────┘└┘  └──┘
doc                                       └────┘    └──┘
txt                                       └────┘    └──┘
par                                       └────┘    └──┘
pid                                             
st                                       └──────────────┘
512  
513  theorem mk_le_mk_iff_dvd_iff {a b : α} : associates.mk a ≤ associates.mk b ↔ a ∣ b :=
id                                           └───────────┘   └───────────┘     
src                                           └───────────┘    └───────────┘      
typ                                          └───────────┘   └───────────┘     
514  iff.intro dvd_of_mk_le_mk mk_le_mk_of_dvd
id   └───────┘ └─────────────┘ └─────────────┘
src  └───────┘ └─────────────┘ └─────────────┘
typ  └───────┘ └─────────────┘ └─────────────┘
515  
516  def prime (p : associates α) : Prop := p ≠ 0 ∧ p ≠ 1 ∧ (∀a b, p ≤ a * b → p ≤ a ∨ p ≤ b)
id                  └────────┘                                         
src                 └────────┘                                                   
typ                 └────────┘                                         
517  
518  lemma prime.ne_zero {p : associates α} (hp : prime p) : p ≠ 0 :=
id                            └────────┘         └───┘      
src                           └────────┘          └───┘        
typ                           └────────┘         └───┘      
519  hp.1
id   └┘
src    
typ  └┘
520  
521  lemma prime.ne_one {p : associates α} (hp : prime p) : p ≠ 1 :=
id                           └────────┘         └───┘      
src                          └────────┘          └───┘        
typ                          └────────┘         └───┘      
522  hp.2.1
id   └┘ 
src     
typ  └┘ 
523  
524  lemma prime.le_or_le {p : associates α} (hp : prime p) {a b : associates α} (h : p ≤ a * b) :
id                             └────────┘         └───┘          └────────┘            
src                            └────────┘          └───┘           └────────┘              
typ                            └────────┘         └───┘          └────────┘            
525    p ≤ a ∨ p ≤ b :=
id           
src            
typ          
526  hp.2.2 a b h
id   └┘     
src     
typ  └┘     
527  
528  lemma exists_mem_multiset_le_of_prime {s : multiset (associates α)} {p : associates α}
id                                              └──────┘  └────────┘         └────────┘ 
src                                             └──────┘  └────────┘          └────────┘
typ                                             └──────┘  └────────┘         └────────┘ 
doc                                             └──────┘
529    (hp : prime p) :
id           └───┘ 
src          └───┘
typ          └───┘ 
530    p ≤ s.prod → ∃a∈s, p ≤ a :=
id       └───┘       
src        └───┘         
typ      └───┘       
doc         └───┘
531  multiset.induction_on s (assume ⟨d, eq⟩, (hp.ne_one (mul_eq_one_iff.1 eq).1).elim) $
id   └───────────────────┘             └┘    └┘└─────┘  └────────────┘       └──┘
src  └───────────────────┘               └┘      └─────┘  └────────────┘       └──┘
typ  └───────────────────┘             └┘    └┘└─────┘  └────────────┘       └──┘
532  assume a s ih h,
id            └┘ 
typ           └┘ 
533    have p ≤ a * s.prod, by simpa using h,
id              └───┘                 
src                └───┘     └──────────┘
typ             └───┘     └──────────┘
doc                  └───┘     └──────────┘
txt                            └──────────┘
par                            └──────────┘
pid                                 └────┘
st                            └────────────┘
534    match hp.le_or_le this with
id           └┘└───────┘ └──┘
src            └───────┘
typ          └┘└───────┘ └──┘
535    | or.inl h := ⟨a, multiset.mem_cons_self a s, h⟩
id       └────┘        └────────────────────┘  
src      └────┘          └────────────────────┘
typ      └────┘        └────────────────────┘  
536    | or.inr h := let ⟨a, has, h⟩ := ih h in ⟨a, multiset.mem_cons_of_mem has, h⟩
id       └────┘     └─┘    └─┘       └┘          └──────────────────────┘
src      └────┘                                     └──────────────────────┘
typ      └────┘     └─┘    └─┘       └┘          └──────────────────────┘
537    end
538  
539  lemma prime_mk (p : α) : prime (associates.mk p) ↔ _root_.prime p :=
id                           └───┘  └───────────┘    └──────────┘ 
src                           └───┘  └───────────┘     └──────────┘
typ                          └───┘  └───────────┘    └──────────┘ 
doc                                                     └──────────┘
540  begin
st   └─────
541    rw [associates.prime, _root_.prime, forall_associated],
id         └──────────────┘  └──────────┘  └───────────────┘
src    └──┘└──────────────┘└┘└──────────┘└┘└───────────────┘
typ    └──┘└──────────────┘└┘└──────────┘└┘└───────────────┘
doc    └──┘                └┘└──────────┘└┘                 
txt    └──┘                └┘            └┘                 
par    └──┘                └┘            └┘                 
pid      └┘                └┘            └┘                 
st   ─────────────────────┘└────────────┘└─────────────────┘└──
542    transitivity,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
st   ─────────────┘└─
543    { apply and_congr, refl,
id             └───────┘
src      └────┘└───────┘  └──┘
typ      └────┘└───────┘  └──┘
doc      └────┘           └──┘
txt      └────┘           └──┘
par      └────┘           └──┘
pid           
st   ───┘└─────────────┘└────┘└─
544      apply and_congr, refl,
id             └───────┘
src      └────┘└───────┘  └──┘
typ      └────┘└───────┘  └──┘
doc      └────┘           └──┘
txt      └────┘           └──┘
par      └────┘           └──┘
pid           
st   ──────────────────┘└────┘└─
545      apply forall_congr, assume a,
id             └──────────┘
src      └────┘└──────────┘  └──────┘
typ      └────┘└──────────┘  └──────┘
doc      └────┘              └──────┘
txt      └────┘              └──────┘
par      └────┘              └──────┘
pid                         └──────┘
st   ─────────────────────┘└────────┘└─
546      exact forall_associated },
id             └───────────────┘
src      └────┘└───────────────┘
typ      └────┘└───────────────┘
doc      └────┘                 
txt      └────┘                 
par      └────┘                 
pid                            
st   ───────────────────────────┘└┘
547    apply and_congr,
id           └───────┘
src    └────┘└───────┘
typ    └────┘└───────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────┘└─
548    { rw [(≠), mk_zero_eq] },
id               └────────┘
src      └──┘└──┘└────────┘└┘
typ      └──┘└──┘└────────┘└┘
doc      └──┘ └──┘          └┘
txt      └──┘ └──┘          └┘
par      └──┘ └──┘          └┘
pid        └┘ └──┘          
st   ───┘└─────┘└──────────┘└┘
549    apply and_congr,
id           └───────┘
src    └────┘└───────┘
typ    └────┘└───────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────┘└─
550    { rw [(≠), ← is_unit_iff_eq_one, is_unit_mk], },
id                 └────────────────┘  └────────┘
src      └──┘└────┘└────────────────┘└┘└────────┘
typ      └──┘└────┘└────────────────┘└┘└────────┘
doc      └──┘ └────┘                  └┘          
txt      └──┘ └────┘                  └┘          
par      └──┘ └────┘                  └┘          
pid        └┘ └────┘                  └┘          
st   ───┘└─────┘└────────────────────┘└──────────┘└───┘
551    apply forall_congr, assume a,
id           └──────────┘
src    └────┘└──────────┘  └──────┘
typ    └────┘└──────────┘  └──────┘
doc    └────┘              └──────┘
txt    └────┘              └──────┘
par    └────┘              └──────┘
pid                       └──────┘
st   ───────────────────┘└────────┘└─
552    apply forall_congr, assume b,
id           └──────────┘
src    └────┘└──────────┘  └──────┘
typ    └────┘└──────────┘  └──────┘
doc    └────┘              └──────┘
txt    └────┘              └──────┘
par    └────┘              └──────┘
pid                       └──────┘
st   ───────────────────┘└────────┘└─
553    rw [mk_mul_mk, mk_le_mk_iff_dvd_iff, mk_le_mk_iff_dvd_iff, mk_le_mk_iff_dvd_iff]
id         └───────┘  └──────────────────┘  └──────────────────┘  └──────────────────┘
src    └──┘└───────┘└┘└──────────────────┘└┘└──────────────────┘└┘└──────────────────┘└┘
typ    └──┘└───────┘└┘└──────────────────┘└┘└──────────────────┘└┘└──────────────────┘└┘
doc    └──┘         └┘                    └┘                    └┘                    └┘
txt    └──┘         └┘                    └┘                    └┘                    └┘
par    └──┘         └┘                    └┘                    └┘                    └┘
pid      └┘         └┘                    └┘                    └┘                    
st   ──────────────┘└────────────────────┘└────────────────────┘└────────────────────┘
554  end
st   └─┘
555  
556  end comm_semiring
557  
558  section integral_domain
559  variable [integral_domain α]
id             └─────────────┘
src            └─────────────┘
typ            └─────────────┘
560  
561  instance : partial_order (associates α) :=
id              └───────────┘  └────────┘ 
src             └───────────┘  └────────┘
typ             └───────────┘  └────────┘ 
562  { le_antisymm := assume a' b',
id                           └┘ └┘
typ                          └┘ └┘
563      quotient.induction_on₂ a' b' $ assume a b ⟨f₁', h₁⟩ ⟨f₂', h₂⟩,
id       └────────────────────┘ └┘ └┘            └─┘  └┘  └─┘  └┘
src      └────────────────────┘
typ      └────────────────────┘ └┘ └┘            └─┘  └┘  └─┘  └┘
564      (quotient.induction_on₂ f₁' f₂' $ assume f₁ f₂ h₁ h₂,
id        └────────────────────┘                  └┘ └┘ └┘ └┘
src       └────────────────────┘
typ       └────────────────────┘                  └┘ └┘ └┘ └┘
565        let ⟨c₁, h₁⟩ := quotient.exact h₁, ⟨c₂, h₂⟩ := quotient.exact h₂ in
id         └─┘      └┘     └────────────┘ └┘       └┘     └────────────┘ └┘
src                        └────────────┘                 └────────────┘
typ        └─┘      └┘     └────────────┘ └┘       └┘     └────────────┘ └┘
566        quotient.sound $ associated_of_dvd_dvd
id         └────────────┘   └───────────────────┘
src        └────────────┘   └───────────────────┘
typ        └────────────┘   └───────────────────┘
567          (h₁ ▸ dvd_mul_of_dvd_left (dvd_mul_right _ _) _)
id                └─────────────────┘  └───────────┘
src               └─────────────────┘  └───────────┘
typ               └─────────────────┘  └───────────┘
568          (h₂ ▸ dvd_mul_of_dvd_left (dvd_mul_right _ _) _)) h₁ h₂
id                └─────────────────┘  └───────────┘
src               └─────────────────┘  └───────────┘
typ               └─────────────────┘  └───────────┘
569    .. associates.preorder }
id        └─────────────────┘
src       └─────────────────┘
typ       └─────────────────┘
570  
571  instance : lattice.order_bot (associates α) :=
id              └───────────────┘  └────────┘ 
src             └───────────────┘  └────────┘
typ             └───────────────┘  └────────┘ 
doc             └───────────────┘
572  { bot := 1,
573    bot_le := assume a, one_le,
id                        └────┘
src                        └────┘
typ                       └────┘
574    .. associates.partial_order }
id        └──────────────────────┘
src       └──────────────────────┘
typ       └──────────────────────┘
575  
576  instance : lattice.order_top (associates α) :=
id              └───────────────┘  └────────┘ 
src             └───────────────┘  └────────┘
typ             └───────────────┘  └────────┘ 
doc             └───────────────┘
577  { top := 0,
578    le_top := assume a, ⟨0, mul_zero a⟩,
id                            └──────┘ 
src                            └──────┘
typ                           └──────┘ 
579    .. associates.partial_order }
id        └──────────────────────┘
src       └──────────────────────┘
typ       └──────────────────────┘
580  
581  theorem zero_ne_one : (0 : associates α) ≠ 1 :=
id                              └────────┘   
src                             └────────┘    
typ                             └────────┘   
582  assume h,
id          
typ         
583  have (0 : α) ~ᵤ 1, from quotient.exact h,
id               └┘         └────────────┘ 
src               └┘         └────────────┘
typ              └┘         └────────────┘ 
584  have (0 : α) = 1, from ((associated_zero_iff_eq_zero 1).1 this.symm).symm,
id                          └─────────────────────────┘     └──┘└───┘ └──┘
src                          └─────────────────────────┘         └───┘ └──┘
typ                         └─────────────────────────┘     └──┘└───┘ └──┘
585  zero_ne_one this
id   └─────────┘ └──┘
src  └─────────┘
typ  └─────────┘ └──┘
586  
587  theorem mul_eq_zero_iff {x y : associates α} : x * y = 0 ↔ x = 0 ∨ y = 0 :=
id                                  └────────┘                  
src                                 └────────┘                       
typ                                 └────────┘                  
588  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
589    (quotient.induction_on₂ x y $ assume a b h,
id      └────────────────────┘              
src     └────────────────────┘
typ     └────────────────────┘              
590      have a * b = 0, from (associated_zero_iff_eq_zero _).1 (quotient.exact h),
id                         └─────────────────────────┘      └────────────┘ 
src                          └─────────────────────────┘      └────────────┘
typ                        └─────────────────────────┘      └────────────┘ 
591      have a = 0 ∨ b = 0, from mul_eq_zero_iff_eq_zero_or_eq_zero.1 this,
id                           └────────────────────────────────┘  └──┘
src                            └────────────────────────────────┘
typ                          └────────────────────────────────┘  └──┘
592      this.imp (assume h, h.symm ▸ rfl) (assume h, h.symm ▸ rfl))
id       └──┘└──┘           └───┘  └─┘            └───┘  └─┘
src          └──┘             └───┘  └─┘              └───┘  └─┘
typ      └──┘└──┘           └───┘  └─┘            └───┘  └─┘
593    (by simp [or_imp_distrib] {contextual := tt})
id               └────────────┘                 └┘
src        └────┘└────────────┘└┘ └────────────┘└┘
typ        └────┘└────────────┘└┘ └────────────┘└┘
doc        └────┘              └┘ └────────────┘  
txt        └────┘              └┘ └────────────┘  
par        └────┘              └┘ └────────────┘  
pid                           └────────────┘  
st        └───────────────────────────────────────┘
594  
595  theorem prod_eq_zero_iff {s : multiset (associates α)} :
id                                 └──────┘  └────────┘ 
src                                └──────┘  └────────┘
typ                                └──────┘  └────────┘ 
doc                                └──────┘
596    s.prod = 0 ↔ (0 : associates α) ∈ s :=
id     └───┘          └────────┘    
src     └───┘          └────────┘    
typ    └───┘          └────────┘    
doc     └───┘
597  multiset.induction_on s (by simp; exact zero_ne_one.symm) $
id   └───────────────────┘                  └──────────────┘
src  └───────────────────┘       └──┘  └────┘└──────────────┘
typ  └───────────────────┘      └──┘  └────┘└──────────────┘
doc                              └──┘  └────┘
txt                              └──┘  └────┘
par                              └──┘  └────┘
pid                                         
st                              └───────────────────────────┘
598    assume a s, by simp [mul_eq_zero_iff, @eq_comm _ 0 a] {contextual := tt}
id                        └─────────────┘   └─────┘                      └┘
src                   └────┘└─────────────┘└┘ └─────┘└───┘ └┘ └────────────┘└┘└─
typ                 └────┘└─────────────┘└┘ └─────┘└───┘└┘ └────────────┘└┘└─
doc                   └────┘               └┘        └───┘ └┘ └────────────┘  └─
txt                   └────┘               └┘        └───┘ └┘ └────────────┘  └─
par                   └────┘               └┘        └───┘ └┘ └────────────┘  └─
pid                                      └┘        └───┘  └────────────┘  
st                   └──────────────────────────────────────────────────────────
599  
src  
typ  
doc  
txt  
par  
pid  
st   
600  theorem irreducible_mk_iff (a : α) : irreducible (associates.mk a) ↔ irreducible a :=
id                                       └─────────┘  └───────────┘    └─────────┘ 
src                                       └─────────┘  └───────────┘     └─────────┘
typ                                      └─────────┘  └───────────┘    └─────────┘ 
doc                                       └─────────┘                     └─────────┘
601  begin
st   └─────
602    simp [irreducible, is_unit_mk],
id           └─────────┘  └────────┘
src    └────┘└─────────┘└┘└────────┘
typ    └────┘└─────────┘└┘└────────┘
doc    └────┘└─────────┘└┘          
txt    └────┘           └┘          
par    └────┘           └┘          
pid                   └┘          
st   ───────────────────────────────┘└─
603    apply and_congr iff.rfl,
id           └───────┘ └─────┘
src    └────┘└───────┘└─────┘
typ    └────┘└───────┘└─────┘
doc    └────┘         
txt    └────┘         
par    └────┘         
pid                  
st   ────────────────────────┘└─
604    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
605    { assume h x y eq,
src      └─────────────┘
typ      └─────────────┘
doc      └─────────────┘
txt      └─────────────┘
par      └─────────────┘
pid      └─────────────┘
st   ───┘└─────────────┘└─
606      have : is_unit (associates.mk x) ∨ is_unit (associates.mk y),
id                                         └─────┘  └───────────┘ 
src      └─────┘                      └┘ └─────┘ └───────────┘ 
typ      └─────┘                     └┘ └─────┘ └───────────┘
doc      └─────┘                      └┘ └─────┘               
txt      └─────┘                      └┘                       
par      └─────┘                      └┘                       
pid      └───┘└┘                      └┘                       
st   ───────────────────────────────────────────────────────────────┘└─
607        from h _ _ (by rw [eq]; refl),
id                           └┘
src        └───┘ └───┘   └──┘└┘└┘└──┘
typ        └───┘└───┘   └──┘└┘└┘└──┘
doc        └───┘ └───┘   └──┘  └┘└──┘
txt        └───┘ └───┘   └──┘  └┘└──┘
par        └───┘ └───┘   └──┘  └┘└──┘
pid        └───┘ └───┘   └───┘  └──────┘
st   ───────────────────┘└─────┘└────┘└─
608      simpa [is_unit_mk] },
id              └────────┘
src      └─────┘└────────┘└┘
typ      └─────┘└────────┘└┘
doc      └─────┘          └┘
txt      └─────┘          └┘
par      └─────┘          └┘
pid                     
st   ──────────────────────┘└┘
609    { refine assume h x y, quotient.induction_on₂ x y (assume x y eq, _),
id                            └────────────────────┘
src      └─────┘      └──────┘└────────────────────┘         └─────────┘
typ      └─────┘      └──────┘└────────────────────┘         └─────────┘
doc      └─────┘      └──────┘                               └─────────┘
txt      └─────┘      └──────┘                               └─────────┘
par      └─────┘      └──────┘                               └─────────┘
pid                  └──────┘                               └─────────┘
st   ─────────────────────────────────────────────────────────────────────┘└─
610      rcases quotient.exact eq.symm with ⟨u, eq⟩,
id              └────────────┘ └─────┘
src      └─────┘└────────────┘└─────┘└───────────┘
typ      └─────┘└────────────┘└─────┘└───────────┘
doc      └─────┘                     └───────────┘
txt      └─────┘                     └───────────┘
par      └─────┘                     └───────────┘
pid                                 └───────────┘
st   ─────────────────────────────────────────────┘└─
611      have : a = x * (y * u), by rwa [mul_assoc, eq_comm] at eq,
id                                 └───────┘  └─────┘
src      └─────┘           └───┘└───────┘└┘└─────┘└─────┘
typ      └─────┘       └───┘└───────┘└┘└─────┘└─────┘
doc      └─────┘             └───┘         └┘       └─────┘
txt      └─────┘             └───┘         └┘       └─────┘
par      └─────┘             └───┘         └┘       └─────┘
pid      └───┘└┘                └┘         └┘       └────┘
st   ─────────────────────────┘          └───────┘└───────┘      └─
612      show is_unit (associates.mk x) ∨ is_unit (associates.mk y),
id                                       └─────┘  └───────────┘ 
src      └───┘                      └┘ └─────┘ └───────────┘ 
typ      └───┘                     └┘ └─────┘ └───────────┘
doc      └───┘                      └┘ └─────┘               
txt      └───┘                      └┘                       
par      └───┘                      └┘                       
pid      └───┘                      └┘                       
st   ─────────────────────────────────────────────────────────────┘└─
613      simpa [is_unit_mk] using h _ _ this }
id              └────────┘             └──┘
src      └─────┘└────────┘└──────┘ └───┘    
typ      └─────┘└────────┘└──────┘└───┘└──┘
doc      └─────┘          └──────┘ └───┘    
txt      └─────┘          └──────┘ └───┘    
par      └─────┘          └──────┘ └───┘    
pid                     └────┘ └───┘    
st   ───────────────────────────────────────┘└─
614  end
st   ──┘
615  
616  lemma eq_of_mul_eq_mul_left :
617    ∀(a b c : associates α), a ≠ 0 → a * b = a * c → b = c :=
id               └────────┘                     
src              └────────┘                           
typ              └────────┘                     
618  begin
st   └─────
619    rintros ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h,
src    └──────────────────────┘
typ    └──────────────────────┘
doc    └──────────────────────┘
txt    └──────────────────────┘
par    └──────────────────────┘
pid           └───────────────┘
st   ─────────────────────────┘└─
620    rcases quotient.exact' h with ⟨u, hu⟩,
id            └─────────────┘ 
src    └─────┘└─────────────┘ └───────────┘
typ    └─────┘└─────────────┘└───────────┘
doc    └─────┘                └───────────┘
txt    └─────┘                └───────────┘
par    └─────┘                └───────────┘
pid                          └───────────┘
st   ──────────────────────────────────────┘└─
621    have hu : a * (b * ↑u) = a * c, { rwa [← mul_assoc] },
id                                       └───────┘
src    └────────┘     └┘       └─────┘└───────┘└┘
typ    └────────┘   └┘     └─────┘└───────┘└┘
doc    └────────┘       └┘        └─────┘         └┘
txt    └────────┘       └┘        └─────┘         └┘
par    └────────┘       └┘        └─────┘         └┘
pid    └─────┘└─┘       └┘           └──┘         
st   ───────────────────────────────┘└──┘└──────────────┘└┘
622    exact quotient.sound' ⟨u, eq_of_mul_eq_mul_left (mt (mk_zero_eq a).2 ha) hu⟩
id           └─────────────┘    └───────────────────┘  └┘  └────────┘     └┘  └┘
src    └────┘└─────────────┘  └┘└───────────────────┘ └┘ └────────┘ └──┘  └┘  └┘
typ    └────┘└─────────────┘ └┘└───────────────────┘ └┘ └────────┘└──┘└┘└┘└┘└┘
doc    └────┘                 └┘                                    └──┘  └┘  └┘
txt    └────┘                 └┘                                    └──┘  └┘  └┘
par    └────┘                 └┘                                    └──┘  └┘  └┘
pid                          └┘                                    └──┘  └┘  
st   ──────────────────────────────────────────────────────────────────────────────┘
623  end
st   └─┘
624  
625  lemma le_of_mul_le_mul_left (a b c : associates α) (ha : a ≠ 0) :
id                                        └────────┘          
src                                       └────────┘            
typ                                       └────────┘          
626    a * b ≤ a * c → b ≤ c
id               
src                  
typ              
627  | ⟨d, hd⟩ := ⟨d, eq_of_mul_eq_mul_left a _ _ ha $ by rwa ← mul_assoc⟩
id                   └───────────────────┘      └┘            └───────┘
src                   └───────────────────┘               └────┘└───────┘
typ                  └───────────────────┘      └┘      └────┘└───────┘
doc                                                       └────┘
txt                                                       └────┘
par                                                       └────┘
pid                                                          └─┘
st                                                       └──────────────┘
628  
629  lemma one_or_eq_of_le_of_prime :
630    ∀(p m : associates α), prime p → m ≤ p → (m = 1 ∨ m = p)
id            └────────┘    └───┘                 
src            └────────┘     └───┘                     
typ           └────────┘    └───┘                 
631  | _ m ⟨hp0, hp1, h⟩ ⟨d, rfl⟩ :=
id                        └─┘
src                          └─┘
typ                       └─┘
632  match h m d (le_refl _) with
id                └─────┘
src               └─────┘
typ               └─────┘
633  | or.inl h := classical.by_cases (assume : m = 0, by simp [this]) $
id     └────┘      └────────────────┘                          └──┘
src    └────┘      └────────────────┘                    └────┘    
typ    └────┘      └────────────────┘                    └────┘└──┘
doc                                                       └────┘    
txt                                                       └────┘    
par                                                       └────┘    
pid                                                               
st                                                       └──────────┘
634    assume : m ≠ 0,
id                
src               
typ               
635    have m * d ≤ m * 1, by simpa using h,
id                                     
src                        └──────────┘
typ                        └──────────┘
doc                           └──────────┘
txt                           └──────────┘
par                           └──────────┘
pid                                └────┘
st                           └────────────┘
636    have d ≤ 1, from associates.le_of_mul_le_mul_left m d 1 ‹m ≠ 0› this,
id                     └──────────────────────────────┘            └──┘
src                    └──────────────────────────────┘           
typ                    └──────────────────────────────┘            └──┘
doc                                                                 
637    have d = 1, from lattice.bot_unique this,
id                     └────────────────┘ └──┘
src                    └────────────────┘
typ                    └────────────────┘ └──┘
638    by simp [this]
id              └──┘
src       └────┘    └┘
typ       └────┘└──┘└┘
doc       └────┘    └┘
txt       └────┘    └┘
par       └────┘    └┘
pid               
st       └───────────┘
639  | or.inr h := classical.by_cases (assume : d = 0, by simp [this] at hp0; contradiction) $
id     └────┘      └────────────────┘                          └──┘
src    └────┘      └────────────────┘                    └────┘    └──────┘  └───────────┘
typ    └────┘      └────────────────┘                    └────┘└──┘└──────┘  └───────────┘
doc                                                       └────┘    └──────┘  └───────────┘
txt                                                       └────┘    └──────┘  └───────────┘
par                                                       └────┘    └──────┘  └───────────┘
pid                                                               └────┘
st                                                       └────────────────────────────────┘
640    assume : d ≠ 0,
id                
src               
typ               
641    have d * m ≤ d * 1, by simpa [mul_comm] using h,
id                                └──────┘        
src                        └─────┘└──────┘└──────┘
typ                        └─────┘└──────┘└──────┘
doc                           └─────┘        └──────┘
txt                           └─────┘        └──────┘
par                           └─────┘        └──────┘
pid                                        └────┘
st                           └───────────────────────┘
642    or.inl $ lattice.bot_unique $ associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
id     └────┘   └────────────────┘   └──────────────────────────────┘            └──┘
src    └────┘   └────────────────┘   └──────────────────────────────┘           
typ    └────┘   └────────────────┘   └──────────────────────────────┘            └──┘
doc                                                                              
643  end
644  
645  end integral_domain
646  
647  end associates